avewright/proofwiki-math huggingface dataset:
Theorem: Third Isomorphism Theorem/Groups

Let $G$ be a group, and let:
:$H, N$ be normal subgroups of $G$
:$N$ be a subset of $H$.
Then:
:$(1): \quad N$ is a normal subgroup of $H$
:$(2): \quad H / N$ is a normal subgroup of $G / N$
:::where $H / N$ denotes the quotient group of $H$ by $N$
:$(3): \quad \dfrac {G / N} {H / N} \cong \dfrac G H$
:::where $\cong$ denotes group isomorphism.

Proof:
From Normal Subgroup which is Subset of Normal Subgroup is Normal in Subgroup, $N$ is a normal subgroup of $H$.
Let $q_H$ denote the quotient mapping from $G$ to $\dfrac G H$.
Let $q_N$ denote the quotient mapping from $G$ to $\dfrac G N$.
Let $\RR$ be the congruence relation defined by $N$ in $G$.
Let $\TT$ be the congruence relation defined by $H$ in $G$.
Thus from Congruence Relation induces Normal Subgroup:
:$q_H = q_\TT$
and:
:$q_N = q_\RR$
where $q_\RR$ and $q_\TT$ denote the quotient epimorphisms induced by $\RR$ and $\TT$ respectively.
We have that:
{{begin-eqn}}
{{eqn | l = \tuple {x, y}
      | o = \in
      | r = \RR
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x N
      | r = y N
      | c = {{Defof|Congruence Modulo Subgroup}}
}}
{{eqn | ll= \leadsto
      | l = x y^{-1}
      | o = \in
      | r = N
      | c = {{Defof|Normal Subgroup}}
}}
{{eqn | ll= \leadsto
      | l = x y^{-1}
      | o = \in
      | r = H
      | c = as $N \subseteq H$
}}
{{eqn | ll= \leadsto
      | l = x H
      | r = y H
      | c = {{Defof|Normal Subgroup}}
}}
{{eqn | l = \tuple {x, y}
      | o = \in
      | r = \TT
      | c = {{Defof|Congruence Modulo Subgroup}}
}}
{{end-eqn}}
That is:
:$\RR \subseteq \TT$
Let $\SS$ be the relation on the quotient group $G / N$ which satisfies:
:$\forall X, Y \in G / N: X \mathrel \SS Y \iff \exists x \in X, y \in Y: x \mathrel \TT y$
That is, by definition of $\TT$:
:$\forall X, Y \in G / N: X \mathrel \SS Y \iff \exists x \in X, y \in Y: x H = y H$
Then by Equivalence Relation induced by Congruence Relation on Quotient Structure is Congruence: Corollary:
:$\SS$ is a congruence relation on $G / N$.
Hence by Congruence Relation on Group induces Normal Subgroup:
:$\SS$ induces a normal subgroup of $G / N$.
{{finish|We need to identify $q_\SS$ with $q_{H / N}$, that is, show that the normal subgroup defined above is $H / N$.}}
Again from Equivalence Relation induced by Congruence Relation on Quotient Structure is Congruence: Corollary:
:there exists a unique isomorphism $\phi$ from $G / N$ to $G / H$ which satisfies:
::$\phi \circ q_\SS \circ q_\RR = q_\TT$
:where $q_\SS$, $q_\RR$ and $q_\TT$ denote the quotient epimorphisms as appropriate.
That is:
:$\phi \circ q_{H / N} \circ q_N = q_H$
and the result follows.
Theorem: Third Isomorphism Theorem/Rings

Let $R$ be a ring.
Let:
:$J, K$ be ideals of $R$
:$J$ be a subset of $K$.
Then:
:$(1): \quad K / J$ is an ideal of $R / J$
::where $K / J$ denotes the quotient ring of $K$ by $J$
:$(2): \quad \dfrac {R / J} {K / J} \cong \dfrac R K$
::where $\cong$ denotes ring isomorphism.

Proof:
By Ideal Contained in Larger Ideal is Ideal of Larger Ideal, $J$ is indeed an ideal of $K$.
Hence $K / J$ is adequately defined.
In Ring Homomorphism whose Kernel contains Ideal, take $\phi: R \to R / K$ to be the quotient epimorphism.
Then (from the same source) its kernel is $K$.
Thus we have that:
:$\phi = \psi \circ \nu$
where $\psi : R / J \to R / K$ is a homomorphism.
This can be illustrated by means of the following commutative diagram:
$\quad\quad \begin{xy}\xymatrix@L+2mu@+1em{
R \ar[dr]_*{\phi}
\ar[r]^*{\nu}
& R / J \ar@{-->}[d]^*{\psi}
\\ 
&
R / K 
}\end{xy}$
As $\phi$ is an epimorphism then from Surjection if Composite is Surjection we have that $\psi$ is a surjection.
So:
:$\Img \psi = \Img \phi = R / K$
and the First Ring Isomorphism Theorem applies.
{{qed}}
Theorem: Inertia Principle

Let $\sequence {a_n}$ be a sequence in $\R$.
Let $a_n \to l$ as $n \to \infty$.
Let $c \in \R$: such that $c < l$.
Then $\exists N \in \N$ such that:
: $\forall n \in \N: n \ge N \implies c < a_n$

Proof:
Pick $\epsilon = l - c > 0$ (as $c < l$).
As $a_n \to l$ as $n \to \infty$, then $\exists N \in \N$ such that:
:$\forall n \in \N: n \ge N \implies \size {a_n - l} < \epsilon$
Equivalently:
:$\forall n \in \N: n \ge N \implies \size {l - a_n} < l - c$
For each $a_n$, either $a_n \ge l$ or $a_n < l$.
If $a_n < l$, then $0 < l - a_n$, so $\size {l - a_n} = l - a_n$.
Then:
{{begin-eqn}}
{{eqn | q = \forall n \in \N
      | l = n
      | o = \ge
      | r = N
}}
{{eqn | ll= \leadsto
      | l = \size {l - a_n}
      | o = \lt
      | r = l - c
}}
{{eqn | ll= \leadsto
      | l = l - a_n
      | o = \lt
      | r = l - c
}}
{{eqn | ll= \leadsto
      | l = a_n
      | o = \gt
      | r = c
}}
{{end-eqn}}
If $a_n \ge l$, and $l > c$, then $a_n > c$.
So:
:$\forall n \in \N: n \ge N \implies a_n > c$
{{qed}}
{{MissingLinks}}
Theorem: Composite of Homomorphisms is Homomorphism/Algebraic Structure

Let:
:$\struct {S_1, \otimes_1, \otimes_2, \ldots, \otimes_n}$
:$\struct {S_2, *_1, *_2, \ldots, *_n}$
:$\struct {S_3, \oplus_1, \oplus_2, \ldots, \oplus_n}$
be algebraic structures.
Let:
:$\phi: \struct {S_1, \otimes_1, \otimes_2, \ldots, \otimes_n} \to \struct {S_2, *_1, *_2, \ldots, *_n}$
:$\psi: \struct {S_2, *_1, *_2, \ldots, *_n} \to \struct {S_3, \oplus_1, \oplus_2, \ldots, \oplus_n}$
be homomorphisms.
Then the composite of $\phi$ and $\psi$ is also a homomorphism.

Proof:
Let $\psi \circ \phi$ denote the composite of $\phi$ and $\psi$.
Then what we are trying to prove is denoted:
:$\paren {\psi \circ \phi}: \struct {S_1, \otimes_1, \otimes_2, \ldots, \otimes_n} \to \struct {S_3, \oplus_1, \oplus_2, \ldots, \oplus_n}$ is a homomorphism.
To prove the above is the case, we need to demonstrate that the morphism property is held by each of the operations $\otimes_1, \otimes_2, \ldots, \otimes_n$ under $\psi \circ \phi$.
Let $\otimes_k$ be one of these operations.
We take two elements $x, y \in S_1$, and put them through the following wringer:
{{begin-eqn}}
{{eqn | l = \map {\paren {\psi \circ \phi} } {x \otimes_k y}
      | r = \map \psi {\map \phi {x \otimes_k y} }
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \map \psi {\map \phi x *_k \map \phi y}
      | c = {{Defof|Morphism Property}}
}}
{{eqn | r = \map \psi {\map \phi x} \oplus_k \map \psi {\map \phi y}
      | c = {{Defof|Morphism Property}}
}}
{{eqn | r = \map {\paren {\psi \circ \phi} } x \oplus_k \map {\paren {\psi \circ \phi} } y
      | c = {{Defof|Composition of Mappings}}
}}
{{end-eqn}}
Disentangling the confusing and tortuous expressions above, we (eventually) see that this shows that the morphism property is indeed held by $\otimes_k$ under $\psi \circ \phi$.
As this holds for any arbitrary operation $\otimes_k$ in $\struct {S_1, \otimes_1, \otimes_2, \ldots, \otimes_n}$, it follows that it holds for all of them.
Thus $\paren {\psi \circ \phi}: \struct {S_1, \otimes_1, \otimes_2, \ldots, \otimes_n} \to \struct {S_3, \oplus_1, \oplus_2, \ldots, \oplus_n}$ is indeed a homomorphism.
{{qed}}
Theorem: Subgroup is Subgroup of Normalizer

Let $G$ be a group.
A subgroup $H \le G$ is a subgroup of its normalizer:
:$H \le G \implies H \le \map {N_G} H$

Proof:
=== Subset of Normalizer ===
First we show that $H$ is a subset of $\map {N_G} H$.
This follows directly from Left Coset Equals Subgroup iff Element in Subgroup:
:$x \in H \implies x H = H$
As $x \in H \implies x^{-1} \in H$ it also follows that $x \in H \implies H x^{-1} = H$.
Thus:
:$x \in H \implies x H x^{-1} = H^x = H$
and so:
:$x \in \map {N_G} H$
So:
:$H \subseteq \map {N_G} H$
as we wanted to show.
{{qed|lemma}}
Theorem: Inclusion Mappings to Topological Sum from Components

Let $\struct {X, \tau_1}$ and $\struct {Y, \tau_2}$ be topological spaces.
Let $\struct {Z, \tau_3}$ be the topological sum of $X$ and $Y$ where $\tau_3$ is the topology generated by $\tau_1$ and $\tau_2$.
Then $\tau_3$ is the finest topology on $Z$ in which the inclusion mappings from $\struct {X, \tau_1}$ and $\struct {Y, \tau_2}$ to $\struct {Z, \tau_3}$ are continuous.

Proof:
{{Recall|Topological Sum|topological sum}}
{{:Definition:Topological Sum}}
Let $\phi_1$ and $\phi_2$ be continuous inclusion mappings from $\struct {X, \tau_1}$ and $\struct {Y, \tau_2}$ to $\struct {Z, \tau_3}$ respectively:
{{begin-eqn}}
{{eqn | l = U \in \tau_3
      | o = \implies
      | r = {\phi_1}^{-1} \sqbrk U \in \tau_1
      | c = 
}}
{{eqn | l = U \in \tau_3
      | o = \implies
      | r = {\phi_2}^{-1} \sqbrk U \in \tau_2
      | c = 
}}
{{end-eqn}}
By definition, $\tau_3$ is the coarsest topology on $Z$ for which every element of $\tau_1$ and $\tau_2$ is open.
Let $\tau_4$ be a finer topology on $Z$ than $\tau_3$.
{{AimForCont}} $\tau_4$ is a topology on $Z$ in which the inclusion mappings from $\struct {X, \tau_1}$ and $\struct {Y, \tau_2}$ to $\struct {Z, \tau_4}$ are continuous.
By definition of finer topology, there exists $V \in \tau_4$ such that $V$ is not a finite intersection of elements of $\tau_1$ and $\tau_2$.
That is, $\tau_4$ cannot be generated by $\tau_1$ and $\tau_2$.
That is:
{{begin-eqn}}
{{eqn | l = {\phi_1}^{-1} \sqbrk V
      | o = \notin
      | r = \tau_1
      | c = 
}}
{{eqn | l = {\phi_2}^{-1} \sqbrk V
      | o = \notin
      | r = \tau_2
      | c = 
}}
{{end-eqn}}
and so the inclusion mappings from $\struct {X, \tau_1}$ and $\struct {Y, \tau_2}$ to $\struct {Z, \tau_4}$ are not continuous.
This contradicts our supposition that they both are.
Hence the result, by Proof by Contradiction.
{{qed}}
{{Proofread}}
Theorem: Principal Ultrafilter is All Sets Containing Cluster Point

Let $S$ be a set.
Let $\powerset S$ denote the power set of $S$.
Let $\FF \subset \powerset S$ be a principal ultrafilter on $S$.
Let its cluster point be $x$.
Then $\FF$ is the set of all subsets $T$ of $S$ such that $x \in T$.

Proof:
We have {{hypothesis}} that the cluster point of $\FF$ is $x$.
Let $A \subseteq S$ such that $x \in A$.
Then, by definition of relative complement:
:$x \notin \relcomp S A$
By definition of cluster point, $x$ is in every element of $\FF$.
But as $x \notin \relcomp S A$, it follows that:
:$\relcomp S A \notin \FF$
So by Ultrafilter Contains Set or Complement:
:$A \in \FF$
Therefore, every $A \subseteq S$ such that $x \in A$ is in $\FF$.
{{AimForCont}} $A \in \FF$ and $x \notin A$.
Then, since $x \in \relcomp S A$, we also have $\relcomp S A \in \FF$ by the above result.
But since:
:$A \cap \relcomp S A = \O$
this contradicts Filter Contains no Disjoint Sets.
Therefore, each $A \in \FF$ has $x \in A$.
Thus, $A \subseteq S$ is in $\FF$ {{iff}} $x \in A$.
{{qed}}
Theorem: Equivalence of Definitions of T4 Space

{{TFAE|def = T4 Space|view = $T_4$ space}}
Let $T = \struct {S, \tau}$ be a topological space.

Proof:
=== Definition by Open Sets implies Definition by Closed Neighborhoods ===
Let $T$ satisfy the definition by open sets of a $T_4$ space.
Let $A$ be a closed set in $T$, and let $U_A$ be an open neighborhood of $A$.
By definition of open neighborhood:
:$A \subseteq U_A$
Let $B := \relcomp S {U_A}$.
By Intersection with Complement is Empty iff Subset:
:$A \cap B = \O$
As $B$ is the complement of $U_A$ in $S$, it is by definition closed in $T$.
Thus $A$ and $B$ are disjoint closed sets in $T$.
Also, from Set Complement inverts Subsets:
:$B \subseteq \relcomp S A$
By assumption, there exist disjoint open sets $U$ and $V$ such that $A \subseteq U$ and $B \subseteq V$.
From Set Intersection Preserves Subsets:
:$B \subseteq \map \complement A \cap V$
Note that the latter set, being an intersection of open sets, is itself open.
Then, from Complement of Complement, De Morgan's Laws: Complement of Union and Set Complement inverts Subsets:
:$A \cup \map \complement V \subseteq U_A$
From Subset of Union we also have:
:$A \subseteq A \cup \map \complement V$
Since $\relcomp S A \cap V$ is open, $A \cup \relcomp S V$ is closed.
Hence we have found a closed neighborhood for $A$ in $U_A$, as desired.
Hence it is concluded that $T$ satisfies the definition by closed neighborhoods of a $T_4$ space.
{{qed|lemma}}
Theorem: Product Space is T2 iff Factor Spaces are T2

:$T$ is a $T_2$ (Hausdorff) space {{iff}} each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_2$ (Hausdorff) space.

Proof:
=== Sufficient Condition ===
{{:Product Space is T2 iff Factor Spaces are T2/Sufficient Condition/Proof 1}}{{qed|lemma}}
Theorem: Product Space is T2 iff Factor Spaces are T2

:$T$ is a $T_2$ (Hausdorff) space {{iff}} each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_2$ (Hausdorff) space.

Proof:
Let $T$ be a $T_2$ space.
As $S_\alpha \ne \O$ we also have $S \ne \O$ by the axiom of choice.
From Subspace of Product Space is Homeomorphic to Factor Space, $\struct {S_\alpha, \tau_\alpha}$ is homeomorphic to a subspace $T_\alpha$ of $T$.
From $T_2$ property is hereditary, $T_\alpha$ is a $T_2$ space.
From $T_2$ Property is Preserved under Homeomorphism, $\struct {S_\alpha, \tau_\alpha}$ is a $T_2$ space.
As $\alpha \in I$ was arbitrary, it follows that each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_2$ space.
Theorem: Product Space is T2 iff Factor Spaces are T2

:$T$ is a $T_2$ (Hausdorff) space {{iff}} each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_2$ (Hausdorff) space.

Proof:
Let $\alpha \in I$.
Let $x, y \in S_\alpha$.
By the Axiom of Choice, there exists $z \in S$.
Define $x', y' \in S$ by:
:$x'_\beta = \begin{cases} z_\beta & \beta \ne \alpha \\ x & \beta = \alpha \end{cases}$
and
:$y'_\beta = \begin{cases} z_\beta & \beta \ne \alpha \\ y & \beta = \alpha \end{cases}$
By definition of a $T_2$ (Hausdorff) space:
:$\exists U, V \in \tau : x' \in U, y' \in V$ and $U \cap V = \O$
Recall that the topology on the product space $T$ is the product topology.
By definition of the product topology the natural basis is a basis for the product topology.
Then:
:$\exists U', V' \in \BB : x' \in U' \subseteq U, y' \in V' \subseteq V$
where $\BB$ is the natural basis for $\tau$.
From Subsets of Disjoint Sets are Disjoint:
:$U' \cap V' = \O$
From Natural Basis of Product Topology:
:$\ds U' = \prod_{\beta \mathop \in I} U_\beta$ where:
::for all $\beta \in I : U_\beta \in \tau_\beta$
::for all but finitely many indices $\beta : U_\beta = X_\beta$
Similarly:
:$\ds V' = \prod_{\beta \mathop \in I} V_\beta$ where:
::for all $\beta \in I : V_\beta \in \tau_\beta$
::for all but finitely many indices $\beta : V_\beta = X_\beta$
From General Case of Cartesian Product of Intersections:
:$\ds \paren {\prod_{\beta \mathop \in I} U_\beta} \bigcap \paren{\prod_{\beta \mathop \in I} V_\beta} = \prod_{\beta \mathop \in I} \paren{U_\beta \cap V_\beta}$
Thus:
:$\ds \prod_{\beta \mathop \in I} \paren{U_\beta \cap V_\beta} = \O$
Now for all $\beta \in I$ such that $\beta \ne \alpha$:
:$z_\beta = x'_\beta \in U_\beta$
and 
:$z_\beta = y'_\beta \in V_\beta$
So:
:$\forall \beta \in I, \beta \ne \alpha : U_\beta \cap V_\beta \ne \O$
From Cartesian Product of Family is Empty iff Factor is Empty it follows that:
:$U_\alpha \cap V_\alpha = \O$
Also we have:
:$x = x'_\alpha \in U_\alpha$
and
:$y = y'_\alpha \in V_\alpha$
Since $U_\alpha$ and $V_\alpha$ are open in $\struct {S_\alpha, \tau_\alpha}$ then $x$ and $y$ are separated by open sets.
Since $x$ and $y$ were arbitrary, then $\struct {S_\alpha, \tau_\alpha}$ is a $T_2$ (Hausdorff) space by definition.
Since $\alpha \in I$ was arbitrary, then for each $\alpha \in I$, $\struct {S_\alpha, \tau_\alpha}$ is a $T_2$ (Hausdorff) space.
{{qed}}
Theorem: Product Space is T2.5 iff Factor Spaces are T2.5

:$T$ is a $T_{2 \frac 1 2}$ space {{iff}} each of $\struct{S_\alpha, \tau_\alpha}$ is a $T_{2 \frac 1 2}$ space.

Proof:
=== Sufficient Condition ===
{{:Product Space is T2.5 iff Factor Spaces are T2.5/Sufficient Condition}}{{qed|lemma}}
Theorem: Product Space is T3 iff Factor Spaces are T3

:$T$ is a $T_3$ space {{iff}} each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_3$ space.

Proof:
=== Sufficient Condition ===
{{:Product Space is T3 iff Factor Spaces are T3/Sufficient Condition}}{{qed|lemma}}
Theorem: Product Space is T3.5 iff Factor Spaces are T3.5

:$T$ is a $T_{3 \frac 1 2}$ space {{iff}} each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_{3 \frac 1 2}$ space.

Proof:
=== Sufficient Condition ===
{{:Product Space is T3.5 iff Factor Spaces are T3.5/Sufficient Condition}}{{qed|lemma}}
Theorem: Factor Spaces are T5 if Product Space is T5

Let $\SS = \family {\struct {S_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$ be an indexed family of topological spaces for $\alpha$ in some indexing set $I$.
Let $\ds T = \struct {S, \tau} = \prod_{\alpha \mathop \in I} \struct {S_\alpha, \tau_\alpha}$ be the product space of $\SS$.
Let $T$ be a $T_5$ space.
Then each of $\struct {S_\alpha, \tau_\alpha}$ is a $T_5$ space.

Proof:
Let $T$ be a $T_5$ space.
Let $\struct {S_\alpha, \tau_\alpha}$ be arbitrary.
By Subspace of Product Space is Homeomorphic to Factor Space:
:$\struct {S_\alpha, \tau_\alpha}$
is homeomorphic to a subspace of $T$.
By $T_5$ Property is Hereditary, this subspace is also $T_5$.
Finally, by $T_5$ Property is Preserved under Homeomorphism:
:$\struct {S_\alpha, \tau_\alpha}$
is a $T_5$ space.
{{qed}}
Category:T5 Spaces
Category:Separation Properties Preserved under Topological Product
Category:Product Spaces
rxxaxwkfgvw3kv0cvf4nmpy03bi4io7
Theorem: T4 Property is not Hereditary

Let $T = \struct {S, \tau}$ be a topological space which is a $T_4$ space.
Let $T_H = \struct {H, \tau_H}$, where $\O \subset H \subseteq S$, be a subspace of $T$.
Then it does not necessarily follow that $T_H$ is a $T_4$ space.

Proof:
Let $T$ be the Tychonoff plank.
Let $T'$ be the deleted Tychonoff plank.
By definition, $T'$ is a subspace of $T$.
From Tychonoff Plank is Normal, $T$ is a normal space.
From Deleted Tychonoff Plank is Not Normal, $T'$ is not a normal space.
{{Recall|Normal Space|normal space|index = 1}}
{{:Definition:Normal Space/Definition 1}}
We have the result $T_1$ Property is Hereditary.
Hence:
:$T'$ is a $T_1$ space.
But because $T'$ is not a normal space it follows that:
:$T'$ is not a $T_4$ space.
Hence the result.
{{qed}}
Category:T4 Spaces
Category:Examples of Hereditary Properties
Category:Separation Properties Preserved in Subspace
b4r7256lse74u18l7g45pd1ks2cl4k9
Theorem: Derivative of Arcsecant Function

:<nowiki>$\dfrac {\map \d {\arcsec x} } {\d x} = \dfrac 1 {\size x \sqrt {x^2 - 1} } = \begin {cases} \dfrac {+1} {x \sqrt {x^2 - 1} } & : 0 < \arcsec x < \dfrac \pi 2 \ (\text {that is: $x > 1$}) \\
\dfrac {-1} {x \sqrt {x^2 - 1} } & : \dfrac \pi 2 < \arcsec x < \pi \ (\text {that is: $x < -1$})  \\
\end{cases}$</nowiki>

Proof:
{{:Graph of Arcsecant Function}}
Let $y = \arcsec x$ where $\size x > 1$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | r = \arcsec x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \sec y
      | c = where $y \in \closedint 0 \pi \land y \ne \dfrac \pi 2$
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d y}
      | r = \sec y \ \tan y
      | c = Derivative of Secant Function
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \dfrac 1 {\sec y \tan y}
      | c = Derivative of Inverse Function
}}
{{eqn | ll= \leadsto
      | l = \paren {\frac {\d y} {\d x} }^2
      | r = \frac 1 {\sec^2 y \ \tan^2 y}
      | c = squaring both sides
}}
{{eqn | r = \frac 1 {\sec^2 y \paren {\sec^2 y - 1} }
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | r = \frac 1 {x^2 \paren {x^2 - 1} }
      | c = Definition of $x$
}}
{{eqn | ll= \leadsto
      | l = \size {\dfrac {\d y} {\d x} }
      | r = \dfrac 1 {\size x \sqrt {x^2 - 1} }
      | c = squaring both sides
}}
{{end-eqn}}
Since $\dfrac {\d y} {\d x} = \dfrac 1 {\sec y \tan y}$, the sign of $\dfrac {\d y} {\d x}$ is the same as the sign of $\sec y \tan y$.
Writing $\sec y \tan y$ as $\dfrac {\sin y} {\cos^2 y}$, it is evident that the sign of $\dfrac {\d y} {\d x}$ is the same as the sign of $\sin y$.
From Sine and Cosine are Periodic on Reals, $\sin y$ is never negative on its domain ($y \in \closedint 0 \pi \land y \ne \pi/2$).
However, by definition of the arcsecant of $x$:
:$0 < \arcsec x < \dfrac \pi 2 \implies x > 1$
:$\dfrac \pi 2 < \arcsec x < \pi \implies x < -1$
Thus:
:<nowiki>$\dfrac {\map \d {\arcsec x} } {\d x} = \dfrac 1 {\size x \sqrt {x^2 - 1} } = \begin{cases} \dfrac {+1} {x \sqrt {x^2 - 1} } & : 0 < \arcsec x < \dfrac \pi 2 \ (\text {that is: $x > 1$})  \\
\dfrac {-1} {x \sqrt {x^2 - 1} } & : \dfrac \pi 2 < \arcsec x < \pi \ (\text {that is: $x < -1$}) \\
\end{cases}$</nowiki>
Hence the result.
{{qed}}
Theorem: Paracompactness is Preserved under Projections

Let $I$ be an indexing set.
Let $\family {\struct {S_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$ be a family of topological spaces indexed by $I$.
Let $\ds \struct {S, \tau} = \prod_{\alpha \mathop \in I} \struct {S_\alpha, \tau_\alpha}$ be the product space of $\family {\struct {S_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$.
Let $\pr_\alpha: \struct {S, \tau} \to \struct {S_\alpha, \tau_\alpha}$ be the projection on the $\alpha$ coordinate.
If $\struct {S, \tau}$ is paracompact, then each of $\struct {S_\alpha, \tau_\alpha}$ is also paracompact.

Proof:
We are given that $\struct {S, \tau}$ is paracompact.
So every open cover of $S$ has an open refinement which is locally finite.
We are given that for each $\alpha \in I$, $\pr_{\alpha}: S \to S_{\alpha}$ is the $\alpha$-th projection.
For each $\alpha \in I$, let $\pr_{\alpha}^\gets: \powerset {S_{\alpha}} \to \powerset S$ be the inverse image mapping induced by $\pr_{\alpha}$
Let $T \subseteq S_\alpha$.
Let $\family {T_i}_{i \mathop \in I}$ be the family of sets defined by:
:$T_i = \begin {cases} T & : i = \alpha \\ S_i & : i \ne \alpha \end {cases}$
By Inverse Image Mapping Induced by Projection, for all $\alpha \in I$, $\pr_\alpha^\gets$ is the mapping defined by:
:$\ds \forall T \subseteq S_i: \map {\pr_{\alpha}^\gets} T = \prod_{i \mathop \in I} T_i$
{{ProofWanted}}
Therefore every open cover of $\struct {S_\alpha, \tau_\alpha}$ has an open refinement which is locally finite.
Hence every $\struct {S_\alpha, \tau_\alpha}$ is paracompact.
{{qed}}
Theorem: Connected Space is Connected Between Two Points

Let $T$ be a topological space which is connected.
Then $T$ is connected between two points.

Proof:
By definition of connected space, $T$ admits no separation.
Therefore, vacuously, every partition has one open containing $t_1, t_2 \in T$, for all $t_1, t_2 \in T$.
That is, for all $t_1, t_2 \in T$, $T$ is connected between $t_1$ and $t_2$.
{{qed}}
Theorem: Equality is Reflexive

:$\forall a: a = a$

Proof:
This proof depends on Leibniz's law:
:$x = y \dashv \vdash \map P x \iff \map P y$
We are trying to prove $a = a$.
Our assertion, then, is:
:$a = a \dashv \vdash \map P a \iff \map P a$
From Law of Identity, $\map P a \iff \map P a$ is a tautology.
Thus $a = a$ is also tautologous, and the theorem holds.
{{qed}}