avewright/proofwiki-math huggingface dataset:
Theorem: Lower Adjoint Preserves All Suprema

Let $\left({S, \preceq}\right)$, $\left({T, \precsim}\right)$ be ordered sets.
Let $d: T \to S$ be an lower adjoint of Galois connection.
Then $d$ preserves all suprema.

Proof:
By definition of lower adjoint
:$\exists g: S \to T: \left({g, d}\right)$ is a Galois connection
Let $X$ be a subset of $T$ such that
:$X$ admits a supremum.
We will prove as lemma 1 that
:$\forall s \in S: s$ is upper bound for $d^\to\left({X}\right) \implies d\left({\sup X}\right) \preceq s$
Let $s \in S$ such that
:$s$ is upper bound for $d^\to\left({X}\right)$
We will prove as sublemma that
:$g\left({s}\right)$ is upper bound for $X$
Let $t \in X$.
By definition of image of set:
:$d \left({t})\right) \in d^\to \left({X}\right)$
By definition of upper bound:
:$d\left({t}\right) \preceq s$
Thus by definition of Galois connection:
:$t \precsim g\left({s}\right)$
This ends the proof of sublemma.
By definition of supremum:
:$\sup X \precsim g\left({t}\right)$
Thus by definition of Galois connection:
:$d\left({\sup X}\right) \preceq t$
This ends the proof of lemma 1.
We will prove as lemma 2 that
:$d\left({\sup X}\right)$ is upper bound for $d^\to\left({X}\right)$
Let $s \in d^\to\left({X}\right)$.
By definition of image of set:
:$\exists t \in T: t \in X \land d\left({t}\right) = s$
By definition of supremum:
:$\sup X$ is upper bound for $X$
By definition of upper bound:
:$t \precsim \sup X$
By definition of Galois connection:
:$d$ is increasing mapping.
Thus by definition of increasing mapping:
:$s \preceq d\left({\sup X}\right)$
This ends the proof of lemma 2.
Thus by definition of supremum:
:$d^\to\left({X}\right)$ admits a supremum
and
:$\sup\left({d^\to\left({X}\right)}\right) = d\left({\sup X}\right)$
Thus by definition:
:$g$ preserves supremum on $X$
Thus by definition:
:$g$ preserves all suprema.
{{qed}}
Theorem: Oscillation at Point (Infimum) equals Oscillation at Point (Limit)

Let $f: D \to \R$ be a real function where $D \subseteq \R$.
Let $x$ be a point in $D$.
Let $N_x$ be the set of neighborhoods of $x$.
Let $\map {\omega_f} x$ be the oscillation of $f$ at $x$ as defined by:
:$\map {\omega_f} x = \inf \set {\map {\omega_f} {I \cap D}: I \in N_x}$
where $\map {\omega_f} {I \cap D}$ is the oscillation of $f$ on a real set $I \cap D$:
:$\map {\omega_f} {I \cap D} = \sup \set {\size {\map f y - \map f z}: y, z \in I \cap D}$
Let $\map {\omega^L_f} x$ be the oscillation of $f$ at $x$ as defined by:
:$\map {\omega^L_f} x = \ds \lim_{h \mathop \to 0^+} \map {\omega_f} {\openint {x - h} {x + h} \cap D}$
Then:
:$\map {\omega_f} x \in \R$ {{iff}} $\map {\omega^L_f} x \in \R$
and, if $\map {\omega_f} x$ and $\map {\omega^L_f} x$ exist as real numbers:
:$\map {\omega_f} x = \map {\omega^L_f} x$

Proof:
=== Lemma ===
{{:Oscillation at Point (Infimum) equals Oscillation at Point (Limit)/Lemma}} {{qed|lemma}}
Theorem: Trisecting the Angle/Parabola

Let $\alpha$ be an angle which is to be trisected.
This can be achieved by means of a parabola.

Proof:
First, notice that because $A$ lies on $\CC_1$:
:$A = \tuple {\cos \angle POQ, \sin \angle POQ}$
This means:
:$B = \tuple {0, \sin \angle POQ}$
Because $C$ is the midpoint of $AB$:
:$C = \tuple {\dfrac {\cos \angle POQ} 2, \sin \angle POQ}$
Because $D$ lies on $\CC_1$:
:$D = \tuple {0, 1}$
and so:
:$E = \tuple {\dfrac {\cos \angle POQ} 2, 1}$
From Equation of Circle, $C_2$ has the equation:
:$\paren {x - \dfrac {\cos \angle POQ} 2}^2 + \paren {y -1}^2 = \dfrac {\cos^2 \angle POQ} 4 + 1$
Because $F$ lies on both $\CC_2$ and $\PP$, we can solve for the $x$-coordinate of $F$:
{{begin-eqn}}
{{eqn | l = \paren {x - \dfrac {\cos \angle POQ} 2}^2 + \paren {2 x^2 - 1}^2
      | r = \dfrac {\cos^2 \angle POQ} 4 + 1
}}
{{eqn | ll= \leadsto
      | l = x^2 - x \cos \angle POQ + \dfrac {\cos^2 \angle POQ} 4 + 4 x^4 - 4 x^2 + 1
      | r = \dfrac {\cos^2 \angle POQ} 4 + 1
}}
{{eqn | ll= \leadsto
      | l = x^2 - x \cos \angle POQ + 4 x^4 - 4 x^2
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = 4 x^4 - 3 x^2 - x \cos \angle POQ
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = x \paren {4 x^3 - 3 x - \cos \angle POQ}
      | r = 0
}}
{{end-eqn}}
Thus $x = 0$ or $4 x^3 - 3 x - \cos \angle POQ = 0$.
This confirms what is obvious by the construction, namely that $\CC_2$ and $\PP$ intersect at the origin.
We can also see that the solution we are after must lie in the first quadrant, where $x \ne 0$.
So there must be one positive $x$ such that:
:$4 x^3 - 3 x = \cos \angle POQ$
By the Triple Angle Formula for Cosine $\cos 3 \theta = 4 \cos^3 \theta - 3 \cos \theta$, it is clear that one solution that works is:
:$x = \map \cos {\dfrac {\angle POQ} 3}$
Because, by construction:
:there is a vertical line through $F$ and $H$
:$H$ lies on the unit circle $\CC_1$
it follows that:
:$H = \tuple {\cos \dfrac {\angle POQ} 3, \sin \dfrac {\angle POQ} 3}$
Therefore:
:$\angle POH = \dfrac {\angle POQ} 3$
{{qed}}
Theorem: All Infima Preserving Mapping is Upper Adjoint of Galois Connection

Let $\struct {S, \preceq}$ be a complete lattice.
Let $\struct {T, \precsim}$ be an ordered set.
Let $g: S \to T$ be an all infima preserving mapping.
Then there exists a mapping $d: T \to S$ such that $\struct {g, d}$ is Galois connection and:
:$\forall t \in T: \map d t = \map \min {g^{-1} \sqbrk {t^\succsim} }$
where:
:$\min$ denotes the minimum
:$g^{-1} \sqbrk {t^\succsim}$ denotes the image of $t^\succsim$ under relation $g^{-1}$
:$t^\succsim$ denotes the upper closure of $t$

Proof:
=== Lemma 1 ===
{{:All Infima Preserving Mapping is Upper Adjoint of Galois Connection/Lemma 1}}{{qed|lemma}}
Let us define a mapping $d: T \to S$ as:
:$\forall t \in T: \map d t := \map \inf {g^{-1} \sqbrk {t^\succsim} }$
Theorem: Image of Inverse Image

Let $S, T$ be sets.
Let $f: S \to T$ be a mapping.
Let $X$ be a subset of $T$.
Then:
:$f \sqbrk {f^{-1} \sqbrk X} \subseteq X$
where:
:$f^{-1} \sqbrk X$ denotes the image of $X$ under the relation $f^{-1}$.

Proof:
Let $x \in f \sqbrk {f^{-1} \sqbrk X}$.
By definition of image of set:
:$\exists y \in S: y \in f^{-1} \sqbrk X \land x = \map f y$
By definition of image of set under relation:
:$\map f y \in X$
Thus $x \in X$
{{qed}}
Theorem: All Suprema Preserving Mapping is Lower Adjoint of Galois Connection

Let $\struct {S, \preceq}$ be an ordered set.
Let $\struct {T, \precsim}$ be a complete lattice.
Let $d: T \to S$ be all suprema preserving mapping.
Then there exists a mapping $g: S \to T$ such that $\tuple {g, d}$ is Galois connection and:
:$\forall s \in S: \map g s = \map \max {d^{-1} \sqbrk {s^\preceq} }$
where
:$\min$ denotes the maximum
:$d^{-1} \sqbrk {s^\preceq}$ denotes the image of $s^\preceq$ under relation $d^{-1}$
:$s^\preceq$ denotes the lower closure of $t$

Proof:
Define a mapping $d: T \to S$:
:$\forall s \in S: \map g s := \map \sup {d^{-1} \sqbrk {s^\preceq} }$
We will prove as lemma 1 that:
:$d$ is an increasing mapping.
Let $x, y \in T$ such that
:$x \precsim y$
By Lower Closure is Increasing:
:$x^\precsim \subseteq y^\precsim$
By Supremum of Lower Closure of Element:
:$\map \sup {x^\precsim} = x$ and $\map \sup {y^\precsim} = y$
By definition of mapping preserves all suprema:
:$d$ preserves the supremum on $x^\precsim$ and $d$ preserves the supremum on $y^\precsim$
By definition of mapping preserves the supremum on set:
:$\map \sup {\map {d^\to} {x^\precsim} } = \map d x$ and $\map \sup {\map {d^\to} {y^\precsim} } = \map d y$
By Image of Subset under Mapping is Subset of Image:
:$\map {d^\to} {x^\precsim} \subseteq \map {d^\to} {y^\precsim}$
Thus by Supremum of Subset:
:$\map d x \preceq \map d y$
This ends the proof of lemma 1.
We will prove as lemma 2 that
:$\forall s \in S: \map g s = \map \max {d^{-1} \sqbrk {s^\preceq} }$
Let $s \in S$.
By definition of $g$:
:$\map g s = \map \sup {d^{-1} \sqbrk {s^\preceq} }$
By Image of Inverse Image:
:$d \sqbrk {d^{-1} \sqbrk {s^\preceq} } \subseteq s^\preceq$
By Supremum of Subset and Supremum of Lower Closure of Element:
:$\map \sup {d \sqbrk {d^{-1} \sqbrk {s^\preceq} } } \preceq \map \sup {s^\preceq} = s$
By definition of lower closure of element:
:$\map \sup {d \sqbrk {d^{-1} \sqbrk {s^\preceq} } } \in s^\preceq$
By definition of complete lattice:
:$d^{-1} \sqbrk {s^\preceq}$ admits a supremum
By definition of mapping preserves the supremum:
:$\map \sup {d \sqbrk {d^{-1} \sqbrk {s^\preceq} } } = \map d {\map g s}$
Thus by definition of image of set:
:$\map g s \in d^{-1} \sqbrk {s^\preceq}$
Thus
:$\map g s = \map \max {d^{-1} \sqbrk {s^\preceq} }$
This ends the proof of lemma 2.
Thus by Galois Connection is Expressed by Maximum:
:$\tuple {g, d}$ is a Galois connection.
Thus by lemma 2:
:$\forall s \in S: \map g s = \map \max {d^{-1} \sqbrk {s^\preceq} }$
{{qed}}
Theorem: Second Derivative at Point of Inflection

Let $f$ be a real function which is twice differentiable on the open interval $\openint a b$.
Let $f$ have a point of inflection at $\xi \in \openint a b$.
Then:
:$\map {f' '} \xi = 0$
where $\map {f' '} \xi$ denotes the second derivative of $f$ at $\xi$.

Proof:
By definition of point of inflection, $f'$ has either a local maximum or a local minimum at $\xi$.
From the Interior Extremum Theorem, it follows that the derivative of $f'$ at $\xi$ is zero, that is:
:$\map {f' '} \xi = 0$
{{qed}}
Theorem: Galois Connection Implies Order on Mappings

Let $\struct {S, \preceq}$, $\struct {T, \precsim}$ be ordered sets.
Let $g: S \to T$ and $d: T \to S$ be mappings such that
:$\tuple {g, d}$ is Galois connection.
Then $d \circ g \preceq I_S$ and $I_T \precsim g \circ d$
where
:$\preceq, \precsim$ denote the orderings on mappings,
:$I_S$ denotes the identity mapping of $S$

Proof:
Let $s \in S$.
By definition of reflexivity:
:$\map g s \precsim \map g s$
By definition of Galois connection:
:$\map d {\map g s} \preceq s$
By definition of composition:
:$\map {\paren {d \circ g} } s \preceq s$
By definition of identity mapping:
:$\map {\paren {d \circ g} } s \preceq \map {I_S} s$
Thus by definition of order on mappings:
:$d \circ g \preceq I_S$
Let $t \in T$.
By definition of reflexivity:
:$\map d t \preceq \map d t$
By definition of Galois connection:
:$t \precsim \map g {\map d t}$
By definition of composition:
:$t \precsim \map {\paren {g \circ d} } t$
By definition of identity mapping:
:$\map {I_T} t \precsim \map {\paren {g \circ d} } t$
Thus by definition of order on mappings:
:$I_T \precsim g \circ d$
{{qed}}
Theorem: Ordering on Mappings Implies Galois Connection

Let $\struct {S, \preceq}$, $\struct {T, \precsim}$ be ordered sets.
Let $g: S \to T$ and $d: T \to S$ be mappings such that:
:$g$ and $d$ are increasing mappings 
and
:$d \circ g \preceq I_S$ and $I_T \precsim g \circ d$
Then
:$\struct {g, d}$ is Galois connection.
where
:$\preceq, \precsim$ denote the orderings on mappings
:$I_S$ denotes the identity mapping of $S$
:$\circ$ denotes the composition of mappings.

Proof:
We will prove that:
:$\forall s \in S, t \in T: t \precsim \map g s \iff \map d t \preceq s$
Let $s \in S, t \in T$.
First implication:
Let
:$t \precsim \map g s$
By definition of increasing mapping:
:$\map d t \preceq \map d {\map g s}$
By definition of ordering on mappings:
:$\map {\paren {d \circ g} } s \preceq \map {I_S} s$
By definition of composition:
:$\map d {\map g s} \preceq \map {I_S} s$
By definition of identity mapping:
:$\map d {\map g s} \preceq s$
Thus by definition of transitivity:
:$\map d t \preceq s$
Second implication:
Let
:$\map d t \preceq s$
By definition of increasing mapping:
:$\map g {\map d t} \precsim \map g s$
By definition of ordering on mappings:
:$\map {I_T} t \precsim \map {\paren {g \circ d} } t$
By definition of composition:
:$\map {I_T} t \precsim \map g {\map d t}$
By definition of identity mapping:
:$t \precsim \map g {\map d t}$
Thus by definition of transitivity:
:$t \precsim \map g s$
Thus by definition:
:$\struct {g, d}$ is Galois connection.
{{qed}}
Theorem: Pi is Transcendental

$\pi$ (pi) is transcendental.

Proof:
Proof by Contradiction:
{{AimForCont}} $\pi$ is not transcendental.
Hence by definition, $\pi$ is algebraic.
Let $\pi$ be the root of a non-zero polynomial with rational coefficients, namely $\map f x$.
Then, $\map g x := \map f {i x} \map f {-i x}$ is also a non-zero polynomial with rational coefficients such that:
:$\map g {i \pi} = 0$
Hence, $i \pi$ is also algebraic.
From the Weaker Hermite-Lindemann-Weierstrass Theorem, $e^{i \pi}$ is transcendental.
However, from Euler's Identity:
:$e^{i \pi} = -1$
which is the root of $\map h z = z + 1$, and so is algebraic.
This contradicts the conclusion that $e^{i \pi}$ is transcendental.
Hence by Proof by Contradiction it must follow that $\pi$ is transcendental.
{{qed}}
Theorem: Gelfond's Constant is Transcendental

'''Gelfond's constant''':
:$e^\pi$
is transcendental.

Proof:
From the Gelfond-Schneider Theorem:
If:
:$\alpha$ and $\beta$ are algebraic numbers such that $\alpha \notin \set {0, 1}$ 
:$\beta$ is either irrational or not wholly real
then $\alpha^\beta$ is transcendental.
We have that:
{{begin-eqn}}
{{eqn | l = i^{-2 i}
      | r = \paren {e^{i \pi / 2} }^{- 2 i}
      | c = 
}}
{{eqn | r = e^{-\pi i^2}
      | c = 
}}
{{eqn | r = e^\pi
      | c = 
}}
{{end-eqn}}
As:
:$i$ is algebraic
:$-2 i$ is algebraic and not wholly real
the conditions of the Gelfond-Schneider Theorem are fulfilled.
Hence the result.
{{qed}}
Theorem: Riemann Surface is Path-Connected

A Riemann surface is path-connected.

Proof:
By definition, a Riemann surface is a complex manifold.
Hence it is connected and locally path-connected.
{{explain|It needs to be established that a complex manifold indeed has both of these properties.}}
{{ProofWanted|A link needed to a page which derives the fact of path-connectedness from connectedness and local path-connectedness.}}
Category:Riemann Surfaces
euw14tot4aq803m48uc9qnzb4b31o5i
Theorem: Radó's Theorem (Riemann Surfaces)

A Riemann surface is second countable.

Proof:
{{ProofWanted}}
{{Namedfor|Tibor Radó|cat = Radó T}}
Theorem: Conformal Isomorphism of Universal Cover of Riemann Surface

The universal cover of a Riemann surface is conformally isomorphic to either:
:the Riemann sphere
:the complex plane
or
:the unit disk.

Proof:
By the Riemann Uniformization Theorem.
{{ProofWanted|Expand into a proof.}}
Category:Riemann Surfaces
h3pzxxsv4n5hnxjbbi8d4y8v7d91ypu
Theorem: Riemann Surface is Metrizable

A Riemann surface is metrizable.

Proof:
Follows {{apriori}} from Riemann Surface admits Metric of Constant Curvature.
{{qed}}
Category:Riemann Surfaces
le3230wb1hxrfa2c8y8dlsqyxoqh0fv
Theorem: Riemann Surface admits Metric of Constant Curvature

A Riemann surface admits a metric of constant curvature.

Proof:
{{ProofWanted}}
Category:Riemann Surfaces
m5kylsa3axmq372rmkcc91uk2txeovp
Theorem: Riemann Sphere is only Elliptic Riemann Surface

The Riemann sphere is the only elliptic Riemann surface (up to conformal isomorphism).

Proof:
{{ProofWanted}}
Category:Riemann Surfaces
cdq7310y4pazt8ulnwuf5vy8g31pgq1
Theorem: Parabolic Riemann Surface is Plane, Punctured Plane or Torus

A parabolic Riemann surface is conformally isomorphic to either:
:the complex plane
:the punctured complex plane $\C \setminus \set 0$
or:
:a torus.

Proof:
{{ProofWanted}}
Category:Riemann Surfaces
a1rl0eigrhpgy6ha6rrzg3u3wsrszus
Theorem: Particle on Curved Surface under no Force moves along Geodesic

Consider a particle $P$ which is constrained to move on a curved surface $C$.
Let $P$ be such that no force acts upon it.
Then $P$ moves along a geodesic.

Proof:
{{ProofWanted|A consequence of Hamilton's Principle in the calculus of variations.}}
Theorem: Sum of Reciprocals of Powers as Euler Product

Let $\zeta$ be the Riemann zeta function.
Let $s \in \C$ be a complex number with real part $\sigma > 1$.
Then:
:$\ds \map \zeta s = \prod_{\text {$p$ prime} } \frac 1 {1 - p^{-s} }$
where the infinite product runs over the prime numbers.

Proof:
By definition of Euler product:
:$\ds \sum_{n \mathop = 1}^\infty a_n n^{-z} = \prod_p \frac 1 {1 - a_p p^{-z} }$
{{iff}} $\ds \sum_{n \mathop = 1}^\infty a_n n^{-z}$ is absolutely convergent.
{{explain|I believe only "if" is true as shown in Product Form of Sum on Completely Multiplicative Function. Or is there a proof for "only if"?}}
For all $n \in \Z_{\ge 1}$, let $a_n = 1$.
From Convergence of P-Series:
:$\ds \sum_{n \mathop = 1}^\infty n^{-z}$ is absolutely convergent
{{iff}}:
:$\cmod z > 1$
It then follows that:
:$\ds \sum_{n \mathop = 1}^\infty \frac 1 {n^z} = \prod_p \frac 1 {1 - p^{-z} }$
{{qed}}
Theorem: Sum of Reciprocals of Powers as Euler Product

Let $\zeta$ be the Riemann zeta function.
Let $s \in \C$ be a complex number with real part $\sigma > 1$.
Then:
:$\ds \map \zeta s = \prod_{\text {$p$ prime} } \frac 1 {1 - p^{-s} }$
where the infinite product runs over the prime numbers.

Proof:
{{Recall|Riemann Zeta Function}}
{{begin-eqn}}
{{eqn | l = \map \zeta s
      | r = \sum_{n \mathop = 1}^\infty \frac 1 {n^s}
      | c = 
}}
{{eqn | r = 1 + \dfrac 1 {2^z} + \dfrac 1 {3^z} + \dfrac 1 {2^{2 z} } + \dfrac 1 {5^z} + \dfrac 1 {2^z 3^z} + \dfrac 1 {7^z} + \dfrac 1 {2^{3 z} } + \dfrac 1 {3^{2 z} } + \cdots
      | c = {{LHS}}
}}
{{end-eqn}}
From Sum of Infinite Geometric Sequence:
:$\dfrac 1 {1 - p^{-z} } = 1 + \dfrac 1 {p^z} + \dfrac 1 {p^{2 z} } + \cdots$
From Convergence of P-Series:
:$\ds \sum_{n \mathop = 1}^\infty n^{-z}$ is absolutely convergent
{{iff}}:
:$\cmod z \gt 1$
Thus:
{{begin-eqn}}
{{eqn | l = \prod_{\text {$p$ prime} } \dfrac 1 {1 - p^{-z} }
      | r = \prod_{\text {$p$ prime} } \paren {1 + \dfrac 1 {p^z} + \dfrac 1 {p^{2 z} } + \dfrac 1 {p^{3 z} } + \cdots}
      | c = 
}}
{{eqn | r = \paren {1 + \dfrac 1 {2^z} + \dfrac 1 {2^{2 z} } + \dfrac 1 {2^{3 z} } + \cdots}
      | c = 
}}
{{eqn | o = 
      | ro= \times
      | r = \paren {1 + \dfrac 1 {3^z} + \dfrac 1 {3^{2 z} } + \dfrac 1 {3^{3 z} } + \cdots}
      | c = 
}}
{{eqn | o = 
      | ro= \times
      | r = \paren {1 + \dfrac 1 {5^z} + \dfrac 1 {5^{2 z} } + \dfrac 1 {5^{3 z} } + \cdots}
      | c = 
}}
{{eqn | o = 
      | ro= \times
      | r = \cdots
      | c = 
}}
{{eqn | r = 1 + \dfrac 1 {2^z} + \dfrac 1 {3^z} + \dfrac 1 {2^{2 z} } + \dfrac 1 {5^z} + \dfrac 1 {2^z 3^z} + \dfrac 1 {7^z} + \dfrac 1 {2^{3 z} } + \dfrac 1 {3^{2 z} } + \cdots
      | c = {{RHS}}
}}
{{end-eqn}}
The Fundamental Theorem of Arithmetic shows that:
:for every integer $n$ such that $n > 1$, $n$ can be expressed as the product of one or more primes, uniquely up to the order in which they appear.
{{qed}}
Theorem: Shift Mapping is Lower Adjoint iff Appropriate Maxima Exist

Let $\struct {S, \preceq}$ be a meet semilattice.
{{TFAE}}
:$(1): \quad \forall x \in S, f: S \to S: \paren {\forall s \in S: \map f s = x \wedge s} \implies f$ is lower adjoint
:$(2): \quad \forall x, t \in S: \max \set {s \in S: x \wedge s \preceq t}$ exists.

Proof:
=== $(1) \implies (2)$ ===
Assume that:
:$\forall x \in S, f: S \to S: \paren {\forall s \in S: \map f s = x \wedge s} \implies f$ is lower adjoint
Let $x, t \in S$.
Define $f: S \to S$:
:$\forall s \in S: \map f s = x \wedge s$
By assumption:
:$f$ is lower adjoint
By definition of lower adjoint:
:$\exists g: S \to S: \struct {g, f}$ is Galois connection
By Galois Connection is Expressed by Maximum:
:$\forall s \in S: \map g s = \map \max {f^{-1} \sqbrk {s^\preceq} }$
Then:
:$\map \max {f^{-1} \sqbrk {t^\preceq} }$ exists.
By definition of image of set:
:$\max \set {s \in S: \map f s \in t^\preceq}$ exists.
By definition of lower closure of element:
:$\max \set {s \in S: x \wedge s \preceq t}$ exists.
{{qed|lemma}}
Theorem: Brouwerian Lattice iff Shift Mapping is Lower Adjoint

Let $\struct {S, \preceq}$ be a lattice.
Then $\struct {S, \preceq}$ is a Brouwerian lattice {{iff}}:
:$\forall x \in S, f: S \to S: \paren {\forall s \in S: \map f s = x \wedge s} \implies f$ is a lower adjoint

Proof:
:$\struct {S, \preceq}$ is a Brouwerian lattice
{{iff}}:
:$\forall x, y \in S: x$ has relative pseudocomplement with respect to $y$ by definition of Brouwerian lattice
{{iff}}:
:$\forall x, y \in S: \max \set {s \in S: x \wedge s \preceq y}$ exists by definition of relative pseudocomplement
{{iff}}:
:$\forall x \in S, f: S \to S: \paren {\forall s \in S: \map f s = x \wedge s} \implies f$ is a lower adjoint by Shift Mapping is Lower Adjoint iff Appropriate Maxima Exist
{{qed}}
Theorem: Brouwerian Lattice is Distributive

Let $\struct {S, \preceq}$ be a Brouwerian lattice.
Then $\struct {S, \preceq}$ is a distributive lattice

Proof:
Let $x, y, z \in S$.
By Brouwerian Lattice iff Shift Mapping is Lower Adjoint:
:$\forall x \in S, f: S \to S: \paren {\forall s \in S: \map f s = x \wedge s} \implies f$ is a lower adjoint
Define a mapping $f: S \to S$:
:$\forall s \in S: \map f s = x \wedge s$
Then:
:$f$ is a lower adjoint
By Lower Adjoint Preserves All Suprema:
:$f$ preserves all suprema
By definition of preserves all suprema:
:$f$ preserves the supremum of $\set {y, z}$
By definition of lattice:
:$\set {y, z}$ admits a supremum
By preserves the supremum of set:
:$\map \sup {\map {f^\to} {\set {y, z} } } = \map f {\sup \set {y, z} }$
Thus
{{begin-eqn}}
{{eqn | l = x \wedge \paren {y \vee z}
      | r = \map f {y \vee z}
      | c = Definition of $f$
}}
{{eqn | r = \map f {\sup \set {y, z} }
      | c = {{Defof|Join (Order Theory)|Join}}
}}
{{eqn | r = \map \sup {\map {f^\to} {\set {y, z} } }
}}
{{eqn | r = \map \sup {\set {\map f y, \map f z} }
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{eqn | r = \sup \set {x \wedge y, x \wedge z}
      | c = Definition of $f$
}}
{{eqn | r = \paren {x \wedge y} \vee \paren {x \wedge z}
      | c = {{Defof|Join (Order Theory)|Join}}
}}
{{end-eqn}}
Thus by definition:
:$\struct {S, \preceq}$ is a distributive lattice
{{qed}}
Theorem: Definite Integral of Reciprocal of Root of a Squared minus x Squared

:$\ds \int_0^x \frac {\d t} {\sqrt{1 - t^2} } = \arcsin x$

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^x \frac {\d t} {\sqrt{1 - t^2} }
      | r = \intlimits {\arcsin \frac t 1} 0 x
      | c = Primitive of $\dfrac 1 {\sqrt {a^2 - x^2} }$, {{Defof|Definite Integral}}
}}
{{eqn | r = \arcsin x - \arcsin 0  
      | c = 
}}
{{eqn | r = \arcsin x 
}}
{{end-eqn}}
{{qed}}
Theorem: Entire Function is Transcendental iff Power Series Expansion is Infinite

Let $f$ be an entire function.
Then $f$ is '''transcendental''' {{iff}} the power series expansion of $f$ has an infinite number of coefficients which are non-zero.

Proof:
{{ProofWanted}}
Category:Entire Functions
miflckvdvsw7isipgspnhc4j3jjh42b
Theorem: Entire Function is Transcendental iff not Complex Polynomial Function

Let $f$ be an entire function.
Then $f$ is '''transcendental''' {{iff}} it is not a complex polynomial function.

Proof:
{{ProofWanted}}
Category:Entire Functions
gyuedjao26bgt0dgqyejduxfigo72tg
Theorem: Complex Function is Entire iff it has Everywhere Convergent Power Series

Let $f: \C \to \C$ be a complex function.
Then $f$ is an '''entire function''' {{iff}} $f$ can be given by an everywhere convergent power series:
:$\ds \map f z = \sum_{n \mathop = 0}^\infty a_n z^n; \quad \lim_{n \mathop \to \infty} \sqrt [n] {\size {a_n} } = 0$

Proof:
{{explain|This needs tightening.}}
Theorem: Brouwerian Lattice is Upper Bounded

Let $\struct {S, \vee, \wedge, \preceq}$ be a Brouwerian lattice.
Then $S$ is upper bounded.

Proof:
By assumption:
:$S \ne \O$
By definition of non-empty set:
:$\exists s: s \in S$
By definition of Brouwerian lattice:
:$s$ has relative pseudocomplement with respect to $s$
By definition of relative pseudocomplement:
:$\max \set {x \in S: s \wedge x \preceq s}$ exists and equals $s \to s$
Let $x \in S$.
By Meet Precedes Operands:
:$s \wedge x \preceq s$
Then:
:$x \in \set {x \in S: s \wedge x \preceq s}$
Thus by definition of maximum:
:$x \preceq s \to s$
Thus by definition:
:$s \to s$ is an upper bound for $S$
Thus by definition:
:$S$ is upper bounded.
{{qed}}