avewright/proofwiki-math huggingface dataset:
Theorem: Existence of Inverse of Class Relation

Let $X$ be a class.
Then there is a class $Z$ such that, for all sets $u, v$:
:$\tuple {u, v} \in Z \iff \tuple {v, u} \in X$
where $\tuple {\cdot, \cdot}$ denotes the Kuratowski formalization of ordered pairs.

Proof:
Let $X$ be arbitrary.
By Axiom $\text B 5$, there is a class $Z_1$ such that:
:$\paren 1 \quad \forall a, w: \tuple {a, w} \in Z_1 \iff a \in X$
Now, by Axiom $\text B 7$, there is a class $Z_2$ such that:
:$\paren 2 \quad \forall u, v, w: \tuple {\tuple {v, w}, u} \in Z_2 \iff \tuple {\tuple {v, u}, w} \in Z_1$
Next, by Axiom $\text B 6$, there is a class $Z_3$ such that:
:$\paren 3 \quad \forall u, v, w: \tuple {\tuple {u, v}, w} \in Z_3 \iff \tuple {\tuple {v, w}, u} \in Z_2$
Finally, by Axiom $\text B 4$, there is a class $Z$ such that:
:$\paren 4 \quad \forall b: b \in Z \iff \exists w: \tuple {b, w} \in Z_3$
We will prove that the $Z$ as defined above satisfies the theorem.
First, choose $a := \tuple {v, u}$ in $\paren 1$, to get:
:$\paren {1'} \quad \forall u, v, w: \tuple {\tuple {v, u}, w} \in Z_1 \iff \tuple {v, u} \in X$
Also, choose $b := \tuple {u, v}$ in $\paren 4$, to get:
:$\paren {4'} \quad \forall u, v: \tuple {u, v} \in Z \iff \exists w: \tuple {\tuple {u, v}, w} \in Z_3$
By Biconditional is Transitive with $\paren 2$ and $\paren 3$, for any $u, v, w$:
:$\paren {2,3} \quad \tuple {\tuple {u, v}, w} \in Z_3 \iff \tuple {\tuple {v, u}, w} \in Z_1$
Now, we can proceed with the equivalence proof.
Suppose $\tuple {v, u} \in X$ for some sets $u, v$.
By the Axiom of Infinity, there exists at least one set $c$.
Then, by $\paren {1'}$:
:$\tuple {\tuple {v, u}, c} \in Z_1$
Thus, by $\paren {2,3}$:
:$\tuple {\tuple {u, v}, c} \in Z_3$
Hence, by $\paren {4'}$, choosing $w := c$:
:$\tuple {u, v} \in Z$
{{qed|lemma}}
Lastly, suppose $\tuple {u, v} \in Z$ for some sets $u, v$.
By $\paren {4'}$, there is some set $w_0$ such that:
:$\tuple {\tuple {u, v}, w_0} \in Z_3$
Then, by $\paren {2,3}$:
:$\tuple {\tuple {v, u}, w_0} \in Z_1$
Thus, by $\paren {1'}$, choosing $w := w_0$:
:$\tuple {v, u} \in X$
{{qed}}
Category:Class Theory
Category:Von Neumann-Bernays-Gödel Set Theory
9a8yajl4fybd5ky14dsiy9kwlrvlb0d
Theorem: Existence of Right Universal Product

For each $m \in \N$, the following is a theorem of von Neumann-Bernays-Gödel set theory:
:$\forall X: \exists Z: \forall v_1, \dotsc, v_m: \forall x: \tuple {\tuple {\dots \tuple {x, v_1}, \dots}, v_m} \in Z \iff x \in X$
Informally, for any class $X$, there is some class $Z$ such that:
:$Z = \paren {\dotsm \paren {X \times V} \times \dotsm} \times V$
where there are $m$ copies of $V$, the universal class, combined with $X$ via the cartesian product.
Note, however, that the formal statement above allows for additional elements of $Z$ which are not of the form as written.

Proof:
We will proceed by induction on $m$.
Importantly, this induction is ''not'' done in the context of NBG.
Rather, it is performed in the metamathematical system in which NBG is formalized.
Theorem: Existence of Left Universal Product

For each $m \in \N_{> 0}$, the following is a theorem of von Neumann-Bernays-Gödel set theory:
:$\forall X: \exists Z: \forall x: \forall v_1, \dotsc, v_m: \sequence {v_1, \dotsc, v_m, x} \in Z \iff x \in X$
where the notation $\sequence {\cdot, \dotsc, \cdot}$ is defined inductively as:
:$\sequence {y_1} := y_1$
:$\sequence {y_1, \dotsc, y_k, y_{k + 1}} := \tuple {\sequence {y_1, \dotsc, y_k}, y_{k + 1}}$
and $\tuple {\cdot, \cdot}$ denotes the Kuratowski formalization of ordered pairs.

Proof:
Let $X$ be arbitrary.
By Axiom $\text B 5$, there is a class $Z$ such that:
:$\forall x, v: \tuple {x, v} \in Z \iff x \in X$
By Existence of Inverse of Class Relation, there is a class $Z'$ such that:
:$\forall v, x: \tuple {v, x} \in Z' \iff \tuple {x, v} \in Z$
Thus, by Biconditional is Transitive:
:$\paren 1 \quad \forall v, x: \tuple {v, x} \in Z' \iff x \in X$
Now, let $v_1, \dotsc, v_m$ be arbitrary.
Substitute $\sequence {v_1, \dotsc, v_m}$ for $v$ in $\paren 1$ to get:
:$\forall x: \forall v_1, \dotsc, v_m: \tuple {\sequence {v_1, \dotsc, v_m}, x} \in Z \iff x \in X$
But, by definition of the notation $\sequence {\cdot, \dotsc, \cdot}$, that is equivalent to:
:$\forall x: \forall v_1, \dotsc, v_m: \sequence {v_1, \dotsc, v_m, x} \in Z \iff x \in X$
{{qed}}
Category:Class Theory
Category:Von Neumann-Bernays-Gödel Set Theory
o20u73z7kn8qw446wdufs9h3u9ug5v4
Theorem: Existence of Middle Universal Product

For each $m \in \N$, the following is a theorem of von Neumann-Bernays-Gödel set theory:
:$\forall X: \exists Z: \forall v_1, \dotsc, v_m: \forall x, y: \sequence {x, v_1, \dotsc, v_m, y} \in Z \iff \tuple {x, y} \in X$
where the notation $\sequence {\cdot, \dotsc, \cdot}$ is defined inductively as:
:$\sequence {y_1} := y_1$
:$\sequence {y_1, \dotsc, y_k, y_{k + 1}} := \tuple {\sequence {y_1, \dotsc, y_k}, y_{k + 1}}$
and $\tuple {\cdot, \cdot}$ denotes the Kuratowski formalization of ordered pairs.

Proof:
In the metatheory in which NBG is formalized, we proceed by induction on $m$.
Theorem: Equal Relative Complements iff Equal Subsets

Let $S$ be a set.
Let $A, B \subseteq S$ be subsets of $S$.
Then:
:$\relcomp S B = \relcomp S A \iff A = B$
where $\complement_S$ denotes the complement relative to $S$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \relcomp S B = \relcomp S A
      | o = \iff
      | r = \relcomp S B \subseteq \relcomp S A \land \relcomp S A \subseteq \relcomp S B
      | c = {{Defof|Set Equivalence}}
}}
{{eqn | o = \iff
      | r = A \subseteq B \land B \subseteq A
      | c = Relative Complement inverts Subsets
}}
{{eqn | o = \iff
      | r = A = B
      | c = {{Defof|Set Equivalence}}
}}
{{end-eqn}}
{{qed}}
Category:Subsets
Category:Relative Complement
jtl5s9ytqu8aoq63yew5vm978ybymzp
Theorem: Relative Complement inverts Subsets of Relative Complement

Let $S$ be a set.
Let $A \subseteq S, B \subseteq S$ be subsets of $S$.
Then:
:$A \subseteq \relcomp S B \iff B \subseteq \relcomp S A$
where $\complement_S$ denotes the complement relative to $S$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = A \subseteq \relcomp S B
      | o = \iff
      | r = \relcomp S {\relcomp S B} \subseteq \relcomp S A
      | c = Relative Complement inverts Subsets
}}
{{eqn | o = \iff
      | r = B \subseteq \relcomp S A
      | c = Relative Complement of Relative Complement
}}
{{end-eqn}}
{{qed}}
Category:Subsets
Category:Relative Complement
iczjq89k6aizwmo5dfwlu6c4qipax1h
Theorem: Sober Space iff Completely Prime Filter is Unique System of Open Neighborhoods

Let $\struct{S, \tau}$ be a topological space.
For each $x \in S$, let:
:$\map \UU x$ denote the system of open neighborhoods of $x$ 
Then $\struct{S, \tau}$ is a sober space {{Iff}}:
:for each completely prime filter $\FF$ in the complete lattice $\struct{\tau, \subseteq}$:
::$\exists ! x \in S : \FF = \map \UU x$

Proof:
Recall by definition of system of open neighborhoods:
:$\forall x \in S : \map \UU x = \set{U \in \tau : x \in U}$
Theorem: Lower Bound of Pell Number

For all $n \in \N$:
:$P_n \ge 2 \paren {1 + \sqrt 2}^{n - 2}$
where:
:$P_n$ is the $n$th Pell number

Proof:
The proof proceeds by induction.
For all $n \in \N$, let $\map P n$ be the proposition:
:$P_n \ge 2 \paren {1 + \sqrt 2}^{n - 2}$
Theorem: Upper Bound of Pell Number

For all $n \in \N$:
:$P_n \le \paren {1 + \sqrt 2}^{n - 1}$
where:
:$P_n$ is the $n$th Pell number

Proof:
The proof proceeds by induction.
For all $n \in \N$, let $\map P n$ be the proposition:
:$P_n \le \paren {1 + \sqrt 2}^{n - 1}$
Theorem: Generalization to Dudeney's Distribution Problem

Suppose $n > 1$ people, each with $a_1, a_2, \dots, a_n$ dollars, redistribute their wealth as follows:
Going in order of their index, each person doubles everyone else's money by giving out their own money.
If they all have the same amount of money after the process, the least (strictly) positive integral solution is:
:$a_j = 2^{j - 1} n + 1, \quad j = 1, \dots, n$
and each person will end up with $2^n$ dollars each.

Proof:
Let us define the total amount of money $S = \ds \sum_{j \mathop = 1}^n a_j$.
Consider the wealth of the $j$th person.
They would see their wealth doubled $j - 1$ times:
:$a_j \to 2^{j - 1} a_j$
Then they would have to give out money to double everyone else's money:
:$2^{j - 1} a_j \to 2^{j - 1} a_j - \paren {S - 2^{j - 1} a_j} = 2^j a_j - S$
since the total amount of money never changes.
Finally, their money will be doubled for $n - j$ more times:
:$2^j a_j - S \to 2^{n - j} \paren {2^j a_j - S} = 2^n a_j - 2^{n - j} S$
Since everyone ends up with the same amount of money, we have:
{{begin-eqn}}
{{eqn | l = 2^n a_j - 2^{n - j} S
      | r = \frac S n
}}
{{eqn | l = a_j
      | r = 2^{-n} \paren {\frac S n + 2^{n - j} S}
}}
{{eqn | r = \frac {S \paren {2^{n - j} n + 1} } {n 2^n}
}}
{{end-eqn}}
Since $a_1 \in \mathbb N$ and $n 2^{n - 1} + 1$ is coprime to both $n$ and $2$ for $n > 1$, by Euclid's Lemma, $S$ must be a multiple of $n 2^n$.
Hence the least positive integral solution is attained at $S = n2^n$.
This shows that $a_j = 2^{j - 1} n + 1$ is the least positive integral solution, and each person will end up with $\dfrac S n = 2^n$ dollars.
{{qed}}
Theorem: Floating-Point Operation may not result in Floating-Point Number

Let a floating-point operation be performed on two floating-point numbers.
Then it is not necessarily the case that the result of that operation is itself a number in floating-point representation.

Proof:
{{ProofWanted|More background needed on how those floating-point operations combine}}
Theorem: Filter Contains Greatest Element

Let $\struct{S, \preceq}$ be an ordered set with greatest element $\top$.
Let $\FF$ be a filter in $\struct{S, \preceq}$.
Then:
:$\top \in \FF$

Proof:
By {{Ordered-set-filter-axiom|1}}:
:$\exists x \in \FF$
By definition of greatest element:
$x \preceq \top$
By {{Ordered-set-filter-axiom|3}}:
:$\top \in \FF$
{{qed}}
Category:Ordered Sets
Category:Filter Theory
Category:Greatest Elements
jyj5woqcv5g0kyliaouddutsw30sdx6
Theorem: System of Open Neighborhoods is a Completely Prime Filter

Let $\struct{S, \tau}$ be a topological space.
Let $x \in S$.
Let $\map \UU x$ denote the system of open neighborhoods of $x$ in $\struct{S, \tau}$.
Then:
:$\map \UU x$ is a completely prime filter in the complete lattice $\struct{\tau, \subseteq}$

Proof:
=== $\map \UU x$ satisfies {{Ordered-set-filter-axiom|1}} ===
We have $x \in S$.
By {{Open-set-axiom|3}}:
:$S \in \tau$
Hence:
:$S \in \map \UU x$
It follows that $\map \UU x$ satisfies {{Ordered-set-filter-axiom|1}}.
{{qed|lemma}}
Theorem: Condition for Equilibrium using Force Polygon

Let $\SS$ be a system of forces $\SS$ act at a point.
Let $\SS$ give rise to a force polygon $A_0 A_1 \ldots A_n A_0$.
Then $\SS$ is in equilibrium {{iff}} $A_n$ and $A_0$ coincide.

Proof:
{{MissingLinks}}
Theorem: Quadratic Form in Two Variables represents Conic Section

A quadratic form in $2$ variables, when put equal to a constant
:$a x^2 + b x y + c y^2 = r$
represents a conic section.

Proof:
It can be seen directly that:
:$a x^2 + b x y + c y^2 = r$
is an instance of an equation for a conic section in Cartesian form:
:$a x^2 + b x y + c y^2 + d x + e y + f = 0$
by setting $f \gets -r$ and equating $d$ and $e$ to zero.
{{qed}}
Theorem: Maximum Speed of Rotation of Plane of Oscillation of Foucault's Pendulum

Let $P$ be a Foucault pendulum.
The maximum angular speed of the plane of oscillation of $P$ occurs at Earth's poles.

Proof:
From Angular Speed of Rotation of Plane of Oscillation of Foucault's Pendulum, the angular speed $\alpha$ of the plane of oscillation of $P$ is given by:
:$\alpha = \omega \sin \lambda$ 
where:
:$\lambda$ denotes the latitude on Earth at which $P$ is located
:$\omega$ denotes the angular speed of rotation of Earth.
So $\size \alpha$ reaches its maximum when $\sin \lambda = \pm 1$.
That is, when $\lambda = \pm 90 \degrees$.
This happens at Earth's poles.
{{qed}}
Theorem: Period of Rotation of Plane of Oscillation of Foucault's Pendulum

Let $P$ be a Foucault pendulum.
The plane of oscillation of $P$ rotates through a full circle in time $T$, where:
:$T = \dfrac D {\sin \lambda}$
where:
:$\lambda$ denotes the latitude on Earth at which $P$ is located
:$D$ denotes the length of a sidereal day.

Proof:
From Angular Speed of Rotation of Plane of Oscillation of Foucault's Pendulum, the angular speed of rotation $\alpha$ of the plane of oscillation of $P$ is given by:
:$\alpha = \omega \sin \lambda$
where:
:$\lambda$ denotes the latitude on Earth at which $P$ is located
:$\omega$ denotes the angular speed of rotation of Earth.
We have:
:$D = \dfrac {2 \pi} \omega$
Hence:
{{begin-eqn}}
{{eqn | l = T
      | r = \dfrac {2 \pi} \alpha
      | c = 
}}
{{eqn | r = \dfrac {2 \pi} {\omega \sin \lambda}
      | c = 
}}
{{eqn | r = \dfrac D {\sin \lambda}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Subtraction of Fractions

Let $a, b, c, d \in \Z$ such that $b d \ne 0$.
Then:
:$\dfrac a b - \dfrac c d = \dfrac {a D - B c} {\lcm \set {b, d} }$
where:
:$B = \dfrac b {\gcd \set {b, d} }$
:$D = \dfrac d {\gcd \set {b, d} }$
:$\lcm$ denotes lowest common multiple
:$\gcd$ denotes greatest common divisor.

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac a b - \dfrac c d
      | r = \dfrac a b + \dfrac {\paren {-c} } d
      | c = 
}}
{{eqn | r = \dfrac {a D + B \paren {-c} } {\lcm \set {b, d} }
      | c = Addition of Fractions
}}
{{eqn | r = \dfrac {a D - B c} {\lcm \set {b, d} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Multiplication of Fractions

Let $a, b, c, d \in \Z$ such that $b d \ne 0$.
Then:
:$\dfrac a b \times \dfrac c d = \dfrac {a c} {b d}$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac a b \times \dfrac c d
      | r = a \times \dfrac 1 b \times c \times \dfrac 1 d
      | c = 
}}
{{eqn | r = a \times c \times \dfrac 1 b \times \dfrac 1 d
      | c = 
}}
{{eqn | r = a c \times \dfrac 1 {b d}
      | c = 
}}
{{eqn | r = \dfrac {a c} {b d}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Division of Fractions

Let $a, b, c, d \in \Z$ such that $b c d \ne 0$.
Then:
:$\dfrac a b \div \dfrac c d = \dfrac {a d} {b c}$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac a b \div \dfrac c d
      | r = \dfrac a b \times \dfrac 1 {c / d}
      | c = 
}}
{{eqn | r = \dfrac a b \times \dfrac d c
      | c = 
}}
{{eqn | r = \dfrac {a d} {b c}
      | c = Multiplication of Fractions
}}
{{end-eqn}}
{{qed}}
Theorem: Subgroup of Free Group is Free Group

Let $G$ be a free group.
Let $H \le G$ be a subgroup of $G$ such that $H$ is not the trivial group.
Then $H$ is also a free group.

Proof:
Let $x \in H$ such that $x$ is not the identity element.
Because $H$ is not the trivial group, such an $x$ always exists.
As $H$ is a subgroup of $G$:
:$x \in G$
where, {{hypothesis}}, $G$ is a free group.
By Element of Free Group can be Expressed Uniquely as Finite Product, $x$ can be expressed uniquely in the form: 
:$a^\alpha b^\beta \dotsm r^\sigma$
where:
:adjacent elements $a, b, \ldots, r$ of $a^\alpha b^\beta \dotsm r^\sigma$ are distinct elements of $G$
:$\alpha, \beta, \ldots, \sigma$ are non-zero integers.
Hence, by definition, $H$ is a free group.
{{qed}}
Theorem: Simpson's Dissection

Let $\omega = e^{2 i \pi / q}$ be a primitive $q$th root of unity.
Let $p \not \equiv 0 \pmod q$.
Let:
:$\ds \map f x = \sum_{n \mathop = 0}^\infty a_n x^n$
Then:
:$\ds \sum_{n \mathop = 0}^\infty a_{n q + p} x^{n q + p} = \dfrac 1 q \sum_{j \mathop = 0}^{q - 1} \omega^{- j p} \map f {\omega^j x}$

Proof:
Expanding the sum on the {{RHS}}, we obtain:
{{begin-eqn}}
{{eqn | l = \dfrac 1 q \sum_{j \mathop = 0}^{q - 1} \omega^{- j p} \map f {\omega^j x}
      | r = \frac 1 q \times \omega^0 \times \paren {a_0 + a_1 x + a_2 x^2 + a_3 x^3 + \cdots}
}}
{{eqn | o = 
      | ro= +
      | r = \frac 1 q \times \omega^{-p} \times \paren {a_0 + a_1 x \omega + a_2 x^2 \omega^2 + a_3 x^3 \omega^3 + \cdots}
}}
{{eqn | o = 
      | ro= +
      | r = \frac 1 q \times \omega^{-2 p} \times \paren {a_0 + a_1 x \paren {\omega^2} + a_2 x^2 \paren {\omega^2}^2 + a_3 x^3 \paren {\omega^2}^3 + \cdots}
}}
{{eqn | o = 
      | ro= +
      | r = \cdots
}}
{{eqn | o = 
      | ro= +
      | r = \frac 1 q \times \omega^{-\paren {q - 1} p} \times \paren {a_0 + a_1 x \paren {\omega^{q - 1} } + a_2 x^2 \paren {\omega^{q - 1} }^2 + a_3 x^3 \paren {\omega^{q - 1} }^3 + \cdots}
}}
{{end-eqn}}
Summing down the $q$ values of the term with exponent n in the array shown above, we obtain:
:$\ds \dfrac 1 q a_n x^n \times \paren {1 + \omega^{1 \paren {n - p} } + \omega^{2 \paren {n - p} } + \omega^{3 \paren {n - p} } + \cdots + \omega^{\paren {q - 1} \paren {n - p} } }$
From Sum of Powers of Primitive Complex Roots of Unity, we have:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 0}^{q - 1} \omega^{j \paren {n - p} }
      | r = 1 + \omega^\paren {n - p} + \omega^{2 \paren {n - p} } + \cdots + \omega^{\paren {q - 1} \paren {n - p} }
      | c = 
}}
{{eqn | r = \begin {cases} q & : q \divides \paren {n - p} \\ 0 & : q \nmid \paren {n - p} \end {cases}
      | c = 
}}
{{end-eqn}}
When $n \equiv p \pmod q$:
:$\ds \dfrac 1 q a_n x^n \times \paren {1 + \omega^{1 \paren {n - p} } + \omega^{2 \paren {n - p} } + \omega^{3 \paren {n - p} } + \cdots + \omega^{\paren {q - 1} \paren {n - p} } } = a_n x^n$
When $n \not \equiv p \pmod q$:
:$\ds \dfrac 1 q a_n x^n \times \paren {1 + \omega^{1 \paren {n - p} } + \omega^{2 \paren {n - p} } + \omega^{3 \paren {n - p} } + \cdots + \omega^{\paren {q - 1} \paren {n - p} } } = 0$
Hence:
{{begin-eqn}}
{{eqn | l = \dfrac 1 q \sum_{j \mathop = 0}^{q - 1} \omega^{- j p} \map f {\omega^j x}
      | r = \sum_{n \mathop = 0}^\infty a_{n q + p} x^{n q + p}
      | c =
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Thomas Simpson|cat = Simpson, T}}
Theorem: Characterization of Locale/Statement 3 Implies Statement 4

Let $L = \struct{S, \preceq}$ be an complete lattice satisfying the infinite join distributive law.
Then:
:$L$ is a Heyting algebra.

Proof:
Let $a, b \in S$.
Let $a \to b = \sup \set{c \in S : a \wedge c \preceq b}$
We have:
{{begin-eqn}}
{{eqn | l = a \wedge \paren{a \to b}
      | r = a \wedge \sup \set{c : a \wedge c \preceq b}
      | c = Definition of $a \to b$
}}
{{eqn | r = \sup \set{a \wedge c : a \wedge c \preceq b}
      | c = Infinite join distributive law
}}
{{eqn | o = \preceq
      | r = b
      | c = {{defof|Supremum of Set}}
}}
{{end-eqn}}
Hence:
:$a \to b$ is the greatest element $c$ such that:
::$c \wedge a \preceq b$
It follows that $a \to b$ is a relative psuedocomplement by definition.
Since $a, b$ were arbitrary, then:
:$\forall a, b \in S : \exists a \to b \in S : a \to b$ is the greatest element $c \in L$ such that $a \wedge c \preceq b$
Hence $L$ is a Heyting algebra by definition.
Theorem: Characterization of Locale/Statement 5 Implies Statement 3

Let $L = \struct{S, \preceq}$ be a complete Brouwerian lattice.
Then:
:$L$ satisfies the infinite join distributive law

Proof:
Let $A \subseteq S$.
Let $a \in S$.
==== Lemma 1 ====
:$\sup \set{a \wedge b : b \in A} \preceq a \wedge \sup A$
==== Proof of Lemma 1 ====
By definition of meet:
:$\forall b \in A : a \wedge b \preceq a, a \wedge b \preceq b$
By definition of upper bound:
:$a$ is an upper bound for $\set{a \wedge b : b \in A}$
By definition of supremum:
:$\sup \set{a \wedge b : b \in A} \preceq a$
From Finer Supremum Precedes Supremum:
:$\sup \set{a \wedge b : b \in A} \preceq \sup A$
By definition of meet:
:$\sup \set{a \wedge b : b \in A} \preceq a \wedge \sup A$
{{qed|lemma}}
==== Lemma 2 ====
:$a \wedge \sup A \preceq \sup \set{a \wedge b : b \in A}$
==== Proof of Lemma 2 ====
By definition of supremum:
:$\forall b \in A : a \wedge b \preceq \sup \set{a \wedge b : b \in A}$
From Relative Pseudocomplement Preserves Order:
:$\forall b \in A : a \to a \wedge b \preceq a \to \sup \set{a \wedge b : b \in A}$
By definition of supremum:
:$\sup \set{a \to a \wedge b : b \in A} \preceq a \to \sup \set{a \wedge b : b \in A}$
From Inequality with Meet Operation is Equivalent to Inequality with Relative Pseudocomplement in Brouwerian Lattice:
:$\forall b \in A : b \preceq a \to a \wedge b$
From Finer Supremum Precedes Supremum:
:$\sup A \preceq \sup \set{a \to a \wedge b : b \in A}$
By {{Ordering-axiom|3}}:
:$\sup A \preceq a \to \sup \set{a \wedge b : b \in A}$
From Inequality with Meet Operation is Equivalent to Inequality with Relative Pseudocomplement in Brouwerian Lattice:
:$a \wedge \sup A \preceq \sup \set{a \wedge b : b \in A}$
{{qed|lemma}}
By {{Ordering-axiom|1}}:
:$a \wedge \sup A = \sup \set{a \wedge b : b \in A}$
Since $A$ and $a$ were arbitrary:
:$\forall A \subseteq S, a \in S : a \wedge \sup A = \sup \set{a \wedge b : b \in A}$
It follows that $L$ satisfies the infinite join distributive law by definition.
Theorem: Equivalence of Definitions of Sober Space

Let $T = \struct{S, \tau}$ be a topological space.
{{TFAE|def=Sober Space}}
=== Definition 1 ===
{{:Definition:Sober Space/Definition 1}}

Proof:
=== Definition 1 implies Definition 2 ===
Let each closed irreducible subspace of $T$ have a unique generic point.
Let $U \ne S$ be a meet-irreducible open set.
Let $F = S \setminus U$.
From Meet-Irreducible Open Set iff Complement is Closed Irreducible Subspace:
:$F$ is closed irreducible subspace
We have {{hypothesis}}:
:$\exists ! x \in S : F = \set x^-$
From Relative Complement inverts Subsets of Relative Complement:
:$\exists ! x \in S : U = S \setminus \set x^-$
The result follows.
{{qed|lemma}}
Theorem: Gaussian Integers are Closed under Addition

The set of Gaussian integers $\Z \sqbrk i$ is closed under addition:
:$\forall x, y \in \Z \sqbrk i: x + y \in \Z \sqbrk i$

Proof:
Let $x$ and $y$ be Gaussian integers.
Then:
{{begin-eqn}}
{{eqn | q = \exists a, b \in \Z
      | l = x
      | r = a + b i
      | c = {{Defof|Gaussian Integer}}
}}
{{eqn | q = \exists c, d \in \Z
      | l = y
      | r = c + d i
      | c = {{Defof|Gaussian Integer}}
}}
{{eqn | ll= \leadsto
      | l = x + y
      | r = \paren {a + c} + \paren {b + d} i
      | c = {{Defof|Complex Addition}}
}}
{{eqn | ll= \leadsto
      | l = x + y
      | o = \in
      | r = \Z \sqbrk i
      | c = Integer Addition is Closed: $a + b \in \Z$ and $c + d \in \Z$
}}
{{end-eqn}}
{{qed}}
Theorem: Gaussian Integers are Closed under Negation

The set of Gaussian integers $\Z \sqbrk i$ is closed under negation:
:$\forall x \in \Z \sqbrk i: -x \in \Z \sqbrk i$

Proof:
Let $x$ be a Gaussian integer.
Then:
{{begin-eqn}}
{{eqn | q = \exists a, b \in \Z
      | l = x
      | r = a + b i
      | c = {{Defof|Gaussian Integer}}
}}
{{eqn | ll= \leadsto
      | l = -x
      | r = -a - b i
      | c = {{Defof|Complex Negation Function}}
}}
{{eqn | ll= \leadsto
      | l = -x
      | o = \in
      | r = \Z \sqbrk i
      | c = {{Defof|Negative Integer}}: $-a \in \Z$, and Integer Subtraction is Closed
}}
{{end-eqn}}
{{qed}}
Category:Gaussian Integers
Category:Negation Functions
Category:Algebraic Closure
159nynevmanced1mp2qrv9nfmprnbas
Theorem: Gaussian Integers are Closed under Subtraction

The set of Gaussian integers $\Z \sqbrk i$ is closed under subtraction:
:$\forall x, y \in \Z \sqbrk i: x - y \in \Z \sqbrk i$

Proof:
Let $x$ and $y$ be Gaussian integers.
Then:
{{begin-eqn}}
{{eqn | l = x - y
      | r = x + \paren {-y}
      | c = {{Defof|Complex Subtraction}}
}}
{{eqn | ll= \leadsto
      | l = x + \paren {-y}
      | o = \in
      | r = \Z \sqbrk i
      | c = Gaussian Integers are Closed under Addition and Gaussian Integers are Closed under Negation
}}
{{eqn | ll= \leadsto
      | l = x - y
      | o = \in
      | r = \Z \sqbrk i
      | c = {{Defof|Complex Subtraction}}
}}
{{end-eqn}}
{{qed}}