avewright/proofwiki-math huggingface dataset:
Theorem: Fontené Theorems/Third

Let $\triangle ABC$ be a triangle.
Let $P$ be an arbitrary point in the plane of $\triangle ABC$.
Let the isogonal conjugate of $P$ {{WRT}} to $\triangle ABC$ be denoted $P^{-1}$.
Let $O$ be the circumcenter of $\triangle ABC$.
Then the pedal circle of $P$ is tangent to the Feuerbach circle of $\triangle ABC$ {{iff}} $O$, $P$, $P^{-1}$ are collinear.

Proof:
{{explain|Too sketchy to be very useful}}
By the Second Fontené Theorem we can prove that the second intersection $Q'$ of the circle $O'$ and the circle $E$ is the anti-Steiner point of $OP^{-1}$.
This means $Q' = Q$ {{iff}} $O P = O P^{-1}$
That is: 
:$O$, $P$ and $P^{-1}$ are collinear.
{{qed}}
Theorem: System of Open Neighborhoods are Equal Iff Singleton Closures are Equal

Let $T = \struct{S, \tau}$ be a topological space.
Let $x, y \in S$ such that $x \ne y$.
Let $\map \UU x$ and $\map \UU y$ denote the system of open neighborhoods of $x$ and $y$ respectively.
Let $\set x^-$ and $\set y^-$ denote the topological closures of $\set x$ and $\set y$ respectively.
Then:
:$\map \UU x = \map \UU y$ {{iff}} $\set x^- = \set y^-$

Proof:
We have
{{begin-eqn}}
{{eqn | l = \map \UU x = \map \UU y
      | o = \leadstoandfrom
      | r = \tau \setminus \map \UU x = \tau \setminus \map \UU y
      | c = Equal Relative Complements iff Equal Subsets
}}
{{eqn | o = \leadsto
      | r = \bigcup \paren{\tau \setminus \map \UU x} = \bigcup \paren{\tau \setminus \map \UU y}
      | c = {{Defof|Set Union}}
}}
{{eqn | o = \leadstoandfrom
      | r = S \setminus \set x^- = S \setminus \set y^-
      | c = Union of Open Sets Not in System of Open Neighborhoods is Complement of Singleton Closure
}}
{{eqn | o = \leadstoandfrom
      | r = \set x^- = \set y^-
      | c = Equal Relative Complements iff Equal Subsets
}}
{{end-eqn}}
It remains to show that if:
:$S \setminus \set x^- = S \setminus \set y^-$ 
then:
:$\tau \setminus \map \UU x = \tau \setminus \map \UU y$ 
Let:
:$S \setminus \set x^- = S \setminus \set y^-$
We have
{{begin-eqn}}
{{eqn | q = \forall U \in \tau 
      | l = U \in \tau \setminus \map \UU x
      | o = \leadstoandfrom
      | r = U \subseteq S \setminus \set x^-
      | c = Open Set Not in System of Open Neighborhoods Iff Subset of Complement of Singleton Closure
}}
{{eqn | o = \leadstoandfrom
      | r = U \subseteq S \setminus \set y^-
      | c = {{Hypothesis}}: $S \setminus \set x^- = S \setminus \set y^-$
}}
{{eqn | o = \leadstoandfrom
      | r = U \in \tau \setminus \map \UU y
      | c = Open Set Not in System of Open Neighborhoods Iff Subset of Complement of Singleton Closure
}}
{{end-eqn}}
By definition of set equality:
:$\tau \setminus \map \UU x = \tau \setminus \map \UU y$ 
The result follows.
{{qed}}
Category:Systems of Open Neighborhoods
6jv08iu0i6mvx7sqnlbxyi3gldg90f4
Theorem: Fontené Theorems/Second

Let $\triangle ABC$ be a triangle.
:480px
Let $P$ be a point moving on a fixed straight line through the circumcenter $O$ of $\triangle ABC$.
Then the pedal circle of $P$ with respect to passes through a fixed point $F$ on the Feuerbach circle of $\triangle ABC$.

Proof:
{{explain|Most of the below completely meaningless because absolutely nothing is explained.}}
By the First Fontené Theorem, the point of contact $Q$ of the circle $E$ and the circle $O'$ is the reflection of a point $F$ which lies on $O P$ with respect to the line $B_1 C_1$.
It is easy to show that $O$ is the orthocenter of triangle $A_1 B_1 C_1$
thus $Q$ is the anti-Steiner point of $d$.
Therefore $Q$ is fixed.
Theorem: Open Set Not in System of Open Neighborhoods Iff Subset of Complement of Singleton Closure

Let $T = \struct{S, \tau}$ be a topological space.
Let $x \in S$.
Let $\map \UU x$ denote the system of open neighborhoods of $x$.
Let $\set x^-$ denote the topological closure of $\set x$.
Then for all $U \in \tau$:
:$U \notin \map \UU x$ {{iff}} $U \subseteq S \setminus \set x^-$

Proof:
First note that by definition of closed set:
:$S \setminus U$ is a closed set
We have:
{{begin-eqn}}
{{eqn | l = U \notin \map \UU x
      | o = \leadstoandfrom
      | r = x \notin U
      | c = {{Defof|System of Open Neighborhoods}}
}}
{{eqn | o = \leadstoandfrom
      | r = \set x \subseteq S \setminus U
      | c = {{Defof|Relative Complement}}
}}
{{eqn | o = \leadstoandfrom
      | r = \set x^- \subseteq S \setminus U
      | c = Closure of Subset of Closed Set of Topological Space is Subset
}}
{{eqn | o = \leadstoandfrom
      | r = U \subseteq S \setminus \set x^-
      | c = Relative Complement inverts Subsets of Relative Complement
}}
{{end-eqn}}
{{qed}}
Category:Systems of Open Neighborhoods
rvnnfde84tamsjkowbdkep3toungj98
Theorem: Complement of Closed Set is Open Set

Let $T = \struct{S, \tau}$ be a topological space.
Let $F \subseteq S$ be a closed set in $T$.
Then:
:$S \setminus F \in \tau$

Proof:
By definition of closed set:
:$\exists U \in \tau : F = S \setminus U$
From Relative Complement inverts Subsets of Relative Complement:
:$U = S \setminus F$
The result follows.
{{qed}}
Category:Closed Sets
Category:Open Sets
7rzvy2si8mmcbrrrx4adcclprcor1c0
Theorem: Union of Open Sets Not in System of Open Neighborhoods is Complement of Singleton Closure

Let $T = \struct{S, \tau}$ be a topological space.
Let $x \in S$.
Let $\map \UU x$ denote the system of open neighborhoods of $x$.
Let $\set x^-$ denote the topological closure of $\set x$.
Then:
:$\bigcup \set{U \in \tau : U \notin \map \UU x} = S \setminus \set x^-$

Proof:
From Open Set Not in System of Open Neighborhoods Iff Subset of Complement of Singleton Closure:
:$\forall U \in \tau : \paren{U \notin \map \UU x \iff U \subseteq S \setminus \set x^-}$
From Union of Subsets is Subset:
:$\bigcup \set{U \in \tau : U \notin \map \UU x} \subseteq S \setminus \set x^-$
From Topological Closure is Closed:
:$\set x^-$ is a closed set
From Complement of Closed Set is Open Set:
:$S \setminus \set x^- \in \tau$
Since $x \notin S \setminus \set x^-$ then:
:$S \setminus \set x^- \in \set{U \in \tau : U \notin \map \UU x}$
From Set is Subset of Union:
:$S \setminus \set x^- \subseteq \bigcup \set{U \in \tau : U \notin \map \UU x}$
By definition of set equality:
:$\bigcup \set{U \in \tau : U \notin \map \UU x} = S \setminus \set x^-$
{{qed}}
Category:Systems of Open Neighborhoods
s7tp6b36maaae5khqd1pnnkiccldwvb
Theorem: Helly's Theorem

Let $A_1, A_2, \ldots, A_r \in \R^n$ be convex sets in real Euclidean $n$-space such that $r > n$.
Let $A_1, A_2, \ldots, A_r$ have the property that every collection of $n + 1$ of $A_1, A_2, \ldots, A_r$ have a point in common.
Then all of $A_1, A_2, \ldots, A_r$ have a point in common.

Proof:
{{ProofWanted}}
{{Namedfor|Eduard Helly|cat = Helly}}
Theorem: Reflexive Riesz Lemma

Let $X$ be a reflexive normed vector space.
Let $Y$ be a proper closed linear subspace of $X$. 
Then $\exists x_\alpha \in X$ such that: 
:$\norm {x_\alpha} = 1$
with:
:$\ds \map d {x_\alpha, Y} = 1$
where $d$ denotes distance to a set.

Proof:
By Existence of Distance Functional, there exists a bounded linear functional $f$ on $X$ such that:
:$\map f y = 0$ for each $y \in Y$
with norm $1$:
:$\norm f = 1$
By the easy direction (sufficiency) of James's Theorem, $\exists x_\alpha \in X$ such that:
:$\norm {x_\alpha} = 1$
and $f$ attains its norm at $x_\alpha$:
:$\size {\map f {x_\alpha} } = 1$
Since $\map f y = 0$ for each $y \in Y$, we have:
:$\forall y \in Y: 1 = \size {\map f {x_\alpha} } = \size {\map f {x_\alpha - y} } \le \norm {x_\alpha - y}$
Taking the infimum over all $y \in Y$, we obtain:
:$\ds 1 \le \inf_{y \mathop \in Y} \norm {x_\alpha - y}$
But $\norm {x_\alpha} = 1$, we obtain:
:$\ds 1 = \inf_{y \mathop \in Y} \norm {x_\alpha - y}$
By definition of distance to a set:
:$\ds \map d {x_\alpha, Y} = 1$
Hence the result.
{{qed}}
Theorem: Integral Representation of Bernoulli Number

Bernoulli numbers can be expressed in integral form as follows:
:$\ds \size {B_{2 n} } = 4 n \int_0^\infty \frac {t^{2 n - 1} } {e^{2 \pi t} - 1} \rd t$
where:
:$B_n$ are the Bernoulli numbers
:$n$ is a positive integer.

Proof:
{{begin-eqn}}
{{eqn | l = \map \zeta s \map \Gamma s
      | r = \int_0^\infty \frac {t^{s - 1} } {e^t - 1} \rd t
      | c = Integral Representation of Riemann Zeta Function in terms of Gamma Function
}}
{{eqn | ll= \leadsto
      | l = \map \zeta {2 n} \map \Gamma {2 n}
      | r = \int_0^\infty \frac {t^{2 n - 1} } {e^t - 1} \rd t
      | c = setting $s:= 2n$
}}
{{eqn | ll= \leadsto
      | l = \paren {-1}^{n + 1} \frac {B_{2 n} 2^{2 n - 1} \pi^{2 n} } {\paren {2 n}!} \paren {2 n - 1}!
      | r = \int_0^\infty \frac {t^{2 n - 1} } {e^t - 1} \rd t
      | c = Riemann Zeta Function at Even Integers, Gamma Function Extends Factorial
}}
{{eqn | ll= \leadsto
      | l = \frac {\size {B_{2 n} } 2^{2 n} \pi^{2 n} } {4 n}
      | r = \int_0^\infty \frac {t^{2 n - 1} } {e^t - 1} \rd t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\size {B_{2 n} } \paren {4 \pi^2}^n} {4 n}
      | r = \int_0^\infty \frac {\paren {2 \pi t}^{2 n - 1} } {e^{2 \pi t} - 1} \paren {2 \pi \rd t}
      | c = $t \to 2 \pi t$ and $\rd t \to 2 \pi \rd t$ and Power of Product
}}
{{eqn | ll= \leadsto
      | l = \size {B_{2 n} } \paren {4 \pi^2}^n
      | r = \paren {4 n} \paren {4 \pi^2}^n  \int_0^\infty \frac {t^{2 n - 1} } {e^{2 \pi t} - 1} \rd t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \size {B_{2 n} }
      | r = 4 n  \int_0^\infty \frac {t^{2 n - 1} } {e^{2 \pi t} - 1} \rd t
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Generic Point of Topological Space

Let $T = \left({S, \tau}\right)$ be a topological space.
Let $x \in S$ be an element of $S$.
{{TFAE|def=Generic Point of Topological Space}}

Proof:
Let $\set x^-$ denote the closure of $\set x$ in $T$.
Let $\map \UU x$ denote the system of open neighborhoods of $x$.
We have:
{{begin-eqn}}
{{eqn | o = 
      | r = \set x^- = S
}}
{{eqn | ll = \leadstoandfrom
      | o = 
      | r = S \setminus \set x^- = \O
      | c = Set Difference with Superset is Empty Set
}}
{{eqn | ll = \leadstoandfrom
      | o = 
      | r = \bigcup \set{U \in \tau : U \notin \map \UU x} = \O
      | c = Union of Open Sets Not in System of Open Neighborhoods is Complement of Singleton Closure
}}
{{eqn | ll = \leadstoandfrom
      | o = 
      | r = \set{U \in \tau : U \notin \map \UU x} = \set {U \in \tau : U = \O}
      | c = Set is Subset of Union and Subset of Empty Set iff Empty
}}
{{eqn | ll = \leadstoandfrom
      | o = 
      | r = \forall U \in \tau : U \ne \O \implies U \in \map \UU x
}}
{{eqn | ll = \leadstoandfrom
      | o = 
      | r = \forall U \in \tau : U \ne \O \implies x \in U
      | c = {{Defof|System of Open Neighborhoods}}
}}
{{end-eqn}}
The result follows.
{{qed}}
Category:Generic Points
4gipwngsdnnrlip2haeji7yr1l4suy7
Theorem: Filter Containing Complements is Not Proper

Let $L = \struct {S, \lor, \land, \preceq}$ be a bounded lattice.
Let $F \subseteq S$ be a filter on $L$.
Suppose there exist $a, b \in F$ such that:
:$b$ is a complement of $a$.
Then:
:$F = S$

Proof:
By filter axiom $\paren 2$:
:$\exists c \in F: c \preceq a \land c \preceq b$
By definition of complement:
:$b \land a = \bot$
Thus, by definition of meet:
:$c \preceq \bot$
Therefore:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = x
      | o = \succeq
      | r = \bot
      | c = {{Defof|Bottom of Lattice}}
}}
{{eqn | o = \succeq
      | r = c
}}
{{eqn | ll = \leadsto
      | q = \forall x \in S
      | l = x
      | o = \in
      | r = F
      | c = Filter Axiom $\paren 3$
}}
{{eqn | ll = \leadsto
      | l = S
      | o = \subseteq
      | r = F
}}
{{end-eqn}}
Hence, by definition of set equality:
:$F = S$
{{qed}}
Category:Bounded Lattices
Category:Filter Theory
acsig9lkpj2q0tzf37rab1m7ceg93zy
Theorem: Meet-Irreducible Open Set iff Complement is Closed Irreducible Subspace

Let $T = \struct{S, \tau}$ be a topological space.
Let $U \in \tau$.
Let $F = S \setminus U$.
Then:
:$U$ is a meet-irreducible open set {{iff}} $F$ is a  closed irreducible subspace

Proof:
We prove the contrapositive statement:
:$F$ is not a  closed irreducible subspace {{iff}} $U$ is not a meet-irreducible open set
Theorem: Meet-Irreducible Open Set iff Complement is Closed Irreducible Subspace/Necessary Condition

Let $T = \struct{S, \tau}$ be a topological space.
Let $U \in \tau$.
Let $F = S \setminus U$.
Let $F$ be a closed irreducible subspace.
Then:
:$U$ is a meet-irreducible open set

Proof:
By definition of closed set:
:$F$ is a closed set
By definition of closed irreducible subspace there exists proper closed subsets $F_1, F_2$ of $F$:
:$F = F_1 \cup F_2$
:$F_1 \subsetneq F$
:$F_2 \subsetneq F$
From Set Complement inverts Subsets and Equal Relative Complements iff Equal Subsets:
:$S \setminus F \subsetneq S \setminus F_1$
:$S \setminus F \subsetneq S \setminus F_2$
From De Morgan's Laws (Set Theory):
:$S \setminus F = S \setminus F_1 \cap S \setminus F_2$
Consider:
:$U_1 = S \setminus F_1$
:$U_2 = S \setminus F_2$
From Complement of Closed Set is Open Set:
:$U_1, U_2 \in \tau$
We have:
:$U \subsetneq U_1$
:$U \subsetneq U_2$
:$U = U_1 \cap U_2$
Hence:
:$U_1 \nsubseteq U$
:$U_2 \nsubseteq U$
:$U = U_1 \cap U_2$
From Characterization of Meet-Irreducible Open Set $U$ is not a meet-irreducible open set.
Theorem: Meet-Irreducible Open Set iff Complement is Closed Irreducible Subspace/Sufficient Condition

Let $T = \struct{S, \tau}$ be a topological space.
Let $U \in \tau$ not be a meet-irreducible open set.
Let $F = S \setminus U$.
Then:
:$F$ is not a  closed irreducible subspace

Proof:
From Characterization of Meet-Irreducible Open Set there exists $V_1, V_2\in \tau$:
:$V_1 \nsubseteq U$
:$V_2 \nsubseteq U$
:$V_1 \cap V_2 \subseteq U$
Let:
:$U_1 = V_1 \cup U$
:$U_2 = V_2 \cup U$
From {{Open-set-axiom|1}}:
:$U_1, U_2 \in \tau$
From Set is Subset of Union:
:$U \subsetneq U_1$
:$U \subsetneq U_2$
We have:
{{begin-eqn}}
{{eqn | l = U_1 \cap U_2 
      | r = \paren{V_1 \cup U} \cap \paren{V_2 \cup U}
}}
{{eqn | r = \paren{U \cap V_1} \cup \paren{U \cap U} \cup \paren{V_2 \cap U} \cup \paren{V_2 \cap V_1}
      | c = Intersection Distributes over Union 
}}
{{eqn | r = \paren{U \cap V_1} \cup U \cup \paren{V_2 \cap U} \cup \paren{V_2 \cap V_1}
      | c = Set Intersection is Idempotent 
}}
{{eqn | r = U
      | c = Union with Superset is Superset 
}}
{{end-eqn}}
From Set Complement inverts Subsets and Equal Relative Complements iff Equal Subsets:
:$S \setminus U_1 \subsetneq S \setminus U$
:$S \setminus U_2 \subsetneq S \setminus U$
From De Morgan's Laws (Set Theory):
:$S \setminus U = S \setminus U_1 \cup S \setminus U_2$
Consider:
:$F_1 = S \setminus U_1$
:$F_2 = S \setminus U_2$
By definition of closed set:
:$F_1, F_2$ and $F$ are closed sets
We have:
:$F_1 \subsetneq F$
:$F_2 \subsetneq F$
:$F_1 \cup F_2 = F$
It follows that $F$ is not a closed irreducible subspace by definition.
Theorem: Equation of Rectangular Hyperbola in Reduced Form

Let $\KK$ be a rectangular hyperbola whose transverse axis and conjugate axis are of length $2 a$.
Let $\KK$ be aligned in a cartesian plane in reduced form.
$\KK$ can be expressed by the equation:
:$x^2 - y^2 = a^2$

Proof:
From Equation of Hyperbola in Reduced Form in Cartesian Frame, a hyperbola can be expressed by the equation:
:$\dfrac {x^2} {a^2} - \dfrac {y^2} {b^2} = 1$
For a rectangular hyperbola:
:$a = b$
Hence $\KK$ can be expressed by the equation:
:$\dfrac {x^2} {a^2} - \dfrac {y^2} {a^2} = 1$
Multiplying both sides by $a^2$
:$x^2 - y^2 = a^2$
{{qed}}
Theorem: Asymptotes to Rectangular Hyperbola

Let $\KK$ be a rectangular hyperbola.
The asymptotes of $\KK$ are perpendicular.

Proof:
Let $\KK$ be embedded in a cartesian plane in reduced form with the equation:
:$x^2 - y^2 = a^2$
From Asymptotes to Hyperbola in Reduced Form, the asymptotes of $\KK$ can be expressed in the form:
:$y = \pm \dfrac b a x$
By definition of a rectangular hyperbola, $\KK$ is such that:
:$a = b$
Hence the asymptotes of $\KK$ can be expressed in the form:
:$y = \pm x$
The slope of $y = x$ is $1$.
The slope of $y = -x$ is $-1$.
We have that:
:$1 = - \dfrac 1 {-1}$
Hence the result, from Condition for Straight Lines in Plane to be Perpendicular: Slope Form.
{{qed}}
Theorem: Frame Homomorphism of Continuous Mapping is Frame Homomorphism

Let $T_1 = \struct{S_1, \tau_1}, T_2 = \struct{S_2, \tau_2}$ be topological spaces.
Let $f : T_1 \to T_2$ be a continuous mapping.
Let $\map \Omega {T_1} = \struct{\tau_1, \subseteq}$ and $\map \Omega {T_2} = \struct{\tau_2, \subseteq}$ denote the frames of $T_1$ and $T_2$ respectively.
Let $\map \Omega f : \map \Omega {T_2} \to \map \Omega {T_1}$ be the frame homomorphism of $f$
Then:
:$\map \Omega f : \map \Omega {T_2} \to \map \Omega {T_1}$ is a frame homomorphism

Proof:
Recall the definition of continuous mapping:
:$f$ is continuous {{iff}} $U \in \tau_2 \implies f^{-1} \sqbrk U \in \tau_1$
By definition of frame homomorphism of $f$:
:$\map \Omega f$ is the inverse image mapping restricted to $\tau_2 \times \tau_1$
By definition of inverse image mapping:
:$\forall U \in \tau_2 : \map {\map \Omega f} U = f^{-1} \sqbrk U$
From Inverse Image Mapping is Mapping:
:$\map \Omega f : \tau_2 \to \tau_1$ is a well-defined mapping.
Theorem: Rotation of Rectangular Hyperbola from Reduced to Standard Form

Let $\KK$ be a rectangular hyperbola embedded in a Cartesian plane in reduced form:
:$x^2 - y^2 = a^2$
Let $\KK$ be rotated $45 \degrees$ clockwise about the origin.
Then $\KK$ is in standard form:
:$x y = c^2$
where $c = \dfrac a {\sqrt 2}$.

Proof:
Let $\tuple {x, y}$ denote an arbitrary point on $\KK$ before rotation.
Let $\tuple {x', y'}$ denote the image of $\tuple {x, y}$ after rotation.
Then:
{{begin-eqn}}
{{eqn | l = \begin {pmatrix} x' \\ y' \end {pmatrix}
      | r = \begin {bmatrix} \map \cos {-45 \degrees} & -\map \sin {-45 \degrees} \\ \map \sin {-45 \degrees} & \map \cos {-45 \degrees} \end {bmatrix} \begin {pmatrix} x \\ y \end {pmatrix}
      | c = Matrix Equation of Plane Rotation: clockwise is negative
}}
{{eqn | r = \begin {bmatrix} \map \cos {45 \degrees} & \map \sin {45 \degrees} \\ -\map \sin {45 \degrees} & \map \cos {45 \degrees} \end {bmatrix} \begin {pmatrix} x \\ y \end {pmatrix}
      | c = Sine Function is Odd, Cosine Function is Even
}}
{{eqn | r = \begin {bmatrix} \dfrac {\sqrt 2} 2 & \dfrac {\sqrt 2} 2 \\ -\dfrac {\sqrt 2} 2 & \dfrac {\sqrt 2} 2 \end {bmatrix} \begin {pmatrix} x \\ y \end {pmatrix}
      | c = {{sin|45}}, {{cos|45}}
}}
{{eqn | r = \begin {bmatrix} \dfrac {\sqrt 2} 2 x + \dfrac {\sqrt 2} 2 y \\ -\dfrac {\sqrt 2} 2 x + \dfrac {\sqrt 2} 2 y \end {bmatrix}
      | c = {{Defof|Matrix Product (Conventional)}}
}}
{{end-eqn}}
Substituting for $x$ and $y$ in $x^2 - y^2 = a^2$:
{{begin-eqn}}
{{eqn | l = \paren {\dfrac {\sqrt 2} 2 x + \dfrac {\sqrt 2} 2 y}^2 - \paren {-\dfrac {\sqrt 2} 2 x + \dfrac {\sqrt 2} 2 y}
      | r = a^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\paren {\dfrac {\sqrt 2} 2}^2 x^2 + 2 \times \paren {\dfrac {\sqrt 2} 2}^2 x y + \paren {\dfrac {\sqrt 2} 2}^2 y^2} - \paren {\paren {\dfrac {\sqrt 2} 2}^2 x^2 - 2 \times \paren {\dfrac {\sqrt 2} 2}^2 x y + \paren {\dfrac {\sqrt 2} 2}^2 y^2}
      | r = a^2
      | c = Square of Sum
}}
{{eqn | ll= \leadsto
      | l = \paren {\dfrac 1 2 x^2 + x y + \dfrac 1 2 y^2} - \paren {\dfrac 1 2 x^2 - x y + \dfrac 1 2 y^2}
      | r = a^2
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = 2 x y
      | r = a^2
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = x y
      | r = \dfrac {a^2} 2
      | c = 
}}
{{eqn | r = \paren {\dfrac a {\sqrt 2} }^2
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Equation of Rectangular Hyperbola in Standard Form/Parametric Form

Let $\KK$ be a rectangular hyperbola in standard form.
$\KK$ can be expressed in parametric form as:
:$\begin {cases} x = c t \\ y = \dfrac c t \end {cases}$

Proof:
Let the point $\tuple {x, y}$ satisfy the equations:
{{begin-eqn}}
{{eqn | l = x
      | r = c t
}}
{{eqn | l = y
      | r = \dfrac c t
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = x y
      | r = c t \times \dfrac c t
      | c = 
}}
{{eqn | r =  c^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Hyperbola in Reduced Form/Cartesian Frame/Parametric Form 2

$K$ can be expressed in parametric form as:
:$\begin {cases} x = a \sec \theta \\ y = b \tan \theta \end {cases}$

Proof:
Let the point $\tuple {x, y}$ satisfy the equations:
{{begin-eqn}}
{{eqn | l = x
      | r = a \sec \theta
}}
{{eqn | l = y
      | r = b \tan \theta
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \frac {x^2} {a^2} - \frac {y^2} {b^2}
      | r = \frac {\paren {a \sec \theta}^2} {a^2} - \frac {\paren {b \tan \theta}^2} {b^2}
      | c = 
}}
{{eqn | r =  \frac {a^2} {a^2} \sec^2 \theta - \frac {b^2} {b^2} \tan^2 \theta
      | c = 
}}
{{eqn | r = \sec^2 \theta - \tan^2 \theta
      | c = 
}}
{{eqn | r = 1
      | c = Difference of Squares of Secant and Tangent
}}
{{end-eqn}}
{{qed}}
Theorem: Frame of Open Sets Functor is Contravariant

Let $\mathbf{Top}$ denote the category of topological spaces.
Let $\mathbf{Frm}$ denote the category of frames.
Then:
:the open sets functor $\mathbf \Omega : \mathbf{Top} \to \mathbf{Frm}$ is a contravariant functor

Proof:
Recall the open sets functor $\mathbf \Omega : \mathbf{Top} \to \mathbf{Frm}$ is defined by:
{{DefineFunctor
|ob = $\map \Omega T := $ the frame of topological space $T$
|mor = $\map \Omega f := $ the frame homomorphism of continuous mapping $f$
}}
Theorem: Frame Homomorphism is Lower Adjoint of Galois Connection

Let $L_1 = \struct{S_1, \preceq_1}, L_2 = \struct{S_2, \preceq_2}$ be frames.
Let $f : L_1 \to L_2$ be a frame homomorphism.
Then there exists a Galois connection $g = \tuple {\upperadjoint g, \loweradjoint g}$:
:the lower adjoint $\loweradjoint g = f$

Proof:
By definition of frame homomorphism:
:$f$ is arbitrary join preserving
From All Suprema Preserving Mapping is Lower Adjoint of Galois Connection:
:there exists a Galois connection $g = \tuple {\upperadjoint g, \loweradjoint g} : \loweradjoint g = f$
{{qed}}
Category:Frame Homomorphisms
Category:Galois Connections
nv22ghy0wdygzwy8xavjwf3hgafc6ef
Theorem: Rational Root Theorem

Let $\map P x$ be a polynomial whose coefficients are all integers:
:$\map P x = a_n x^n + a_{n - 1} x^{n - 1} + \cdots + a_1 x + a_0$
where $a_n \ne 0$ and $a_0 \ne 0$.
Let the polynomial equation $\map P x = 0$ have a root which is a rational number expressed in canonical form as $\dfrac p q$.
Then:
:the leading coefficent $a_n$ of $\map P x$ is divisible by $q$
:the constant term $a_0$ of $\map P x$ is divisible by $p$.

Proof:
{{Recall|Canonical Form of Rational Number}}
{{:Definition:Canonical Form of Rational Number}}
We have {{hypothesis}} that $\dfrac p q$ is a root of $P$.
Hence:
{{begin-eqn}}
{{eqn | l = \map P {\dfrac p q}
      | r = 0
      | c = {{Defof|Root of Polynomial}}
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = a_n \paren {\dfrac p q}^n + a_{n - 1} \paren {\dfrac p q}^{n - 1} + \cdots + a_1 \paren {\dfrac p q} + a_0
      | c = Definition of $P$
}}
{{eqn | n = 1
      | r = a_n p^n + a_{n - 1} p^{n - 1} q + \cdots + a_1 p q^{n - 1} + a_0 q^n
      | c = multiplying both sides by $q^n$
}}
{{eqn | ll= \leadsto
      | l = -a_0 q^n
      | r = a_n p^n + a_{n - 1} p^{n - 1} q + \cdots + a_1 p q^{n - 1}
      | c = subtracting $a_0 q^n$ from both sides
}}
{{eqn | r = p \paren {a_n p^{n - 1} + a_{n - 1} p^{n - 2} q + \cdots + a_1 q^{n - 1} }
      | c = Distributive Laws of Arithmetic
}}
{{end-eqn}}
By the closure of addition and multiplication over the integers:
:$a_n p^{n - 1} + a_{n - 1} p^{n - 2} q + \cdots + a_1 q^{n - 1} \in \Z$
By Euclid's Lemma, either:
:$p \divides q^n$
or:
:$p \divides a_0$
where $\divides$ denotes divisibility.
Because $p \nmid q$ we have that:
:$p \nmid q^n$
Hence:
:$p \divides a_0$
{{qed|lemma}}
Then:
{{begin-eqn}}
{{eqn | l = 0
      | r = a_n p^n + a_{n - 1} p^{n - 1} q + \cdots + a_1 p q^{n - 1} + a_0 q^n
      | c = from $(1)$
}}
{{eqn | ll= \leadsto
      | l = -a_n p^n
      | r = q \paren {a_{n - 1} p^{n - 1} + \cdots + a_1 p q^{n - 2} + a_0 q^{n - 1} }
      | c = 
}}
{{end-eqn}}
Using the same argument as for $p \divides a_0$, it follows that:
:$q \divides a_n$
{{qed}}