avewright/proofwiki-math huggingface dataset:
Theorem: Center of Mass of Uniform Circular Arc

Let $\WW$ be a wire of uniform density.
Let $\WW$ be bent into the shape of the arc of a circle $\CC$ of radius $r$ subtending an angle of $2 \alpha$ from the center of $\CC$.
Then the center of mass of $\WW$ is the point $\dfrac {r \sin \alpha} \alpha$ from the center of $\CC$.

Proof:
Let $\lambda$ be the linear mass density of the wire.
From definition of radian, the total length of the wire is:
:$L = 2 \alpha r$
Therefore, the total mass of the wire is:
:$M = L \lambda = 2 \alpha r \lambda$
Arrange a coordinate system so that:
:the wire is within the $x$-$y$ plane
:the center of the circle containing the arc of the wire is coincident with the origin.
From the parametric equation of circle, the wire can now be represented as:
:$\forall \theta \in \closedint {-\alpha} \alpha : \WW = \tuple {r \cos \theta, r \sin \theta}$
From the definition of center of mass, we have:
:$\ds M \overline {\mathbf r} = \int_V \map \rho {\mathbf r} \mathbf r \rd V$
Therefore,
{{begin-eqn}}
{{eqn | l = \overline {\mathbf r}
      | r = \frac 1 M \int_V \map \rho {\mathbf r} \mathbf r \rd V
}}
{{eqn | r = \frac 1 {2 \alpha r \lambda} \int_{-\alpha}^\alpha \lambda \tuple {r \cos \theta, r \sin \theta} r \rd \theta
      | c = $M = 2 \alpha r \lambda$, $\map \rho {\mathbf r} = \lambda$, $\mathbf r = \tuple {r \cos \theta, r \sin \theta}$, and $\d V = r \rd \theta$
}}
{{eqn | r = \frac r {2 \alpha} \int_{-\alpha}^\alpha \tuple {\cos \theta, \sin \theta} \rd \theta
      | c = $\lambda$ and $r$ are constant
}}
{{eqn | r = \frac r {2 \alpha} \intlimits {\tuple {\sin \theta, -\cos \theta} } {-\alpha} \alpha
      | c = Primitive of Cosine Function and Primitive of Sine Function
}}
{{eqn | r = \frac r {2 \alpha} \tuple {2 \sin \alpha, 0}
      | c = Sine Function is Odd and Cosine Function is Even
}}
{{eqn | r = \tuple {\frac {r \sin \alpha} \alpha, 0}
}}
{{end-eqn}}
{{qed}}
Theorem: Center of Mass of Uniform Circular Sector

Let $\WW$ be a uniform lamina in the shape of the sector of a circle $\CC$ of radius $r$ of an angle of $2 \alpha$.
Then the center of mass of $\PP$ is the point $\dfrac {2 r \sin \alpha} {3 \alpha}$ from the center of $\CC$.

Proof:
Let the sector have a constant area mass density of $\sigma$.
Let $\CC$ lie in the $x$-$y$ plane of a Cartesian coordinate system.
Let the center of $\CC$ coincide with the origin.
Let the $x$-axis bisect the sector.
We have the center of mass equation:
:$\ds M \bar {\mathbf r} = \int_V \map \rho {\mathbf r} \mathbf r \rd V$
The total mass $M$ of the sector is its area times $\sigma$:
{{begin-eqn}}
{{eqn | l = M
      | r = \sigma \frac {r^2 \paren {2 \alpha} } 2
}}
{{eqn | r = \sigma \alpha r^2
}}
{{end-eqn}}
Divide the sector into a set of concentric circular arcs with a radii $r'$ and widths $\d r$.
The infinitesimal area of each arc is
:$\d V = 2 \alpha r' \d r$
From Center of Mass of Uniform Circular Arc, the center of mass of each arc is:
:$\mathbf r = \tuple {\dfrac {r' \sin \alpha} \alpha, 0}$
So:
{{begin-eqn}}
{{eqn | l = \overline {\mathbf r}
      | r = \frac 1 M \int_V \map \rho {\mathbf r} \mathbf r \rd V
}}
{{eqn | r = \frac 1 {\sigma \alpha r^2} \int_0^r \sigma \tuple {\frac {r' \sin \alpha} \alpha, 0} 2 \alpha r' \d r'
}}
{{eqn | r = \frac {2 \sin \alpha} {\alpha r^2} \int_0^r \tuple {r'^2, 0} \rd r'
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac {2 \sin \alpha} {\alpha r^2} \tuple {\frac 1 3 r^3, 0}
      | c = Primitive of Power
}}
{{eqn | r = \tuple {\frac {2 r \sin \alpha} {3 \alpha}, 0}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Moment of Inertia of Uniform Rectangular Lamina through Midpoint about Perpendicular Axis

Let $\LL$ be a uniform lamina of mass $M$ in the shape of a rectangle whose sides are of length $2 a$ and $2 b$.
Let $\AA$ be the straight line through the centroid of $\LL$ perpendicular to $\LL$.
Then the moment of inertia $\II$ of $\LL$ about $\AA$ is given by:
:$\II = \dfrac {M \paren {a^2 + b^2} } 3$

Proof:
Let $\AA_a$ be the straight line:
:through the centroid of $\LL$
:in the plane of $\LL$
:perpendicular to the side of $\LL$ of length $2 a$.
Let $\AA_b$ be the straight line:
:through the centroid of $\LL$
:in the plane of $\LL$
:perpendicular to the side of $\LL$ of length $2 b$.
Let $\II_a$ be the moment of inertia of $\LL$ about $\AA_a$.
Let $\II_b$ be the moment of inertia of $\LL$ about $\AA_b$.
We note that $\AA$ is perpendicular to both $\AA_a$ and $\AA_b$.
We have:
{{begin-eqn}}
{{eqn | l = \II_a
      | r = \dfrac {M a^2} 3
      | c = Moment of Inertia of Uniform Rectangular Lamina about Axis in Plane Bisecting Lamina
}}
{{eqn | l = \II_b
      | r = \dfrac {M b^2} 3
      | c = Moment of Inertia of Uniform Rectangular Lamina about Axis in Plane Bisecting Lamina
}}
{{eqn | l = \II
      | r = \II_a + \II_b
      | c = Perpendicular Axes Theorem
}}
{{eqn | ll= \leadsto
      | l = \II
      | r = \dfrac {M a^2} 3 + \dfrac {M b^2} 3
      | c = 
}}
{{eqn | r = \dfrac {M \paren {a^2 + b^2} } 3
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Moment of Inertia of Uniform Elliptical Lamina through Midpoint about Perpendicular Axis

Let $\LL$ be a uniform lamina of mass $M$ in the shape of a ellipse whose axes are of length $2 a$ and $2 b$.
Let $\AA$ be the straight line through the centroid of $\LL$ perpendicular to $\LL$.
Then the moment of inertia $\II$ of $\LL$ about $\AA$ is given by:
:$\II = \dfrac {M \paren {a^2 + b^2} } 4$

Proof:
Let $\AA_a$ be the straight line coinciding with the axis of $\LL$ of length $2 a$.
Let $\AA_b$ be the straight line coinciding with the axis of $\LL$ of length $2 b$.
Let $\II_a$ be the moment of inertia of $\LL$ about $\AA_a$.
Let $\II_b$ be the moment of inertia of $\LL$ about $\AA_b$.
We note that $\AA$ is perpendicular to both $\AA_a$ and $\AA_b$.
We have:
{{begin-eqn}}
{{eqn | l = \II_a
      | r = \dfrac {M b^2} 4
      | c = Moment of Inertia of Uniform Rectangular Lamina about Axis in Plane Bisecting Lamina
}}
{{eqn | l = \II_b
      | r = \dfrac {M a^2} 4
      | c = Moment of Inertia of Uniform Rectangular Lamina about Axis in Plane Bisecting Lamina
}}
{{eqn | l = \II
      | r = \II_a + \II_b
      | c = Perpendicular Axes Theorem
}}
{{eqn | ll= \leadsto
      | l = \II
      | r = \dfrac {M a^2} 4 + \dfrac {M b^2} 4
      | c = 
}}
{{eqn | r = \dfrac {M \paren {a^2 + b^2} } 4
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Category of Lattices is Category

Let $\mathbf{Lat}$ denote the category of lattices.
Then:
:$\mathbf{Lat}$ is a metacategory

Proof:
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
For any two lattice homomorphisms their composition (in the usual set theoretic sense) is again a lattice homomorphism by Composite Lattice Homomorphisms is Lattice Homomorphism.
For any lattice $\struct{L, \vee, \wedge, \preceq}$, we have the identity mapping $\operatorname{id}_L$.
From Identity Mapping is Lattice Homomorphism we have $\operatorname{id}_L$ is a lattice homomorphism.
By Identity Mapping is Left Identity and Identity Mapping is Right Identity, this is the identity morphism for $\struct{L, \vee, \wedge, \preceq}$.
Finally by Composition of Mappings is Associative, the associative property is satisfied.
Hence $\mathbf{Lat}$ is a metacategory.
{{qed}}
Theorem: Composite Lattice Homomorphisms is Lattice Homomorphism

Let $L_1 = \struct{A_1, \vee_1, \wedge_1, \preceq_1}$, $L_2 = \struct{A_2, \vee_2, \wedge_2, \preceq_2}$ and $L_3 = \struct{A_3, \vee_3, \wedge_3, \preceq_3}$ be lattices.
Let $\phi_1: L_1 \to L_2$ and $\phi_2: L_2 \to L_3$ be lattice homomorphisms.
Let $\phi_2 \circ \phi_1 : A_1 \to A_3$ be the composite mapping of $\phi_1$ and $\phi_2$  
Then:
:$\phi_2 \circ \phi_1$ is a lattice homomorphism of $L_1$ to $L_3$

Proof:
Follows immediately from Composite of Homomorphisms is Homomorphism
{{qed}}
Category:Lattice Homomorphisms
om3nw5mtzzsvjroe9k0fllt2g207brh
Theorem: Identity Mapping is Lattice Homomorphism

Let $L = \struct{A, \vee, \wedge, \preceq}$ be a lattice.
Let $\operatorname{id}_A$ denote the identity mapping on $A$.
Then:
:$\operatorname{id}_A$ is a lattice homomorphism of $L$ to $L$

Proof:
Follows from Identity Mapping is Automorphism applied to $\struct{A, \vee}$ and $\struct{A, \wedge}$.
{{qed}}
Category:Lattice Homomorphisms
o3t1i1hguvpqxsl9jh1hima14sabg0l
Theorem: Equivalence of Definitions of Lattice Isomorphism/Definition 1 Implies Definition 2

Let $L_1 = \struct {A_1, \vee_1, \wedge_1, \preceq_1}$ and $L_2 = \struct {A_2, \vee_2, \wedge_2, \preceq_2}$ be lattices.
Let $\phi : L_1 \to L_2$ be a bijective lattice homomorphism.
Then:
:$\phi : \struct{A_1, \preceq_1} \to \struct{A_2, \preceq_2}$ is an order isomorphism by definition.

Proof:
From Inverse of Bijective Lattice Homomorphism is Bijective Lattice Homomorphism:
:$\phi^{-1}: L_2 \to L_1$ is a bijective lattice homomorphism.
From Lattice Homomorphism is Order-Preserving:
:$\phi : \struct{A_1, \preceq_1} \to \struct{A_2, \preceq_2}$ and $\phi^{-1} : \struct{A_2, \preceq_2} \to \struct{A_1, \preceq_1}$ are order-preserving
Hence $\phi : \struct{A_1, \preceq_1} \to \struct{A_2, \preceq_2}$ is an order isomorphism by definition.
Theorem: Carnot's Theorem

All reversible heat engines operating between the same temperatures are equally efficient.

Proof:
{{ProofWanted}}
{{Namedfor|Nicolas Léonard Sadi Carnot|cat = Carnot, Sadi}}
Theorem: Inverse of Bijective Lattice Homomorphism is Bijective Lattice Homomorphism

Let $L_1 = \struct {A_1, \vee_1, \wedge_1, \preceq_1}$ and $L_2 = \struct {A_2, \vee_2, \wedge_2, \preceq_2}$ be lattices.
Let $\phi: L_1 \to L_2$ be a bijective lattice homomorphism.
Let $\phi^{-1} : A_2 \to A_1$ be the inverse of $\phi : A_1 \to A_2$.
Then:
:$\phi^{-1} : L_2 \to L_1$ is a bijective lattice homomorphism

Proof:
From Inverse of Bijection is Bijection:
:$\phi^{-1}$ is a bijection
It remains to show that $\phi^{-1}$ is a lattice homomorphism.
Theorem: Number of Eigenvalues of Square Complex Matrix

Let $\mathbf A$ be a square matrix of order $n$ over the complex numbers $\C$.
Then $\mathbf A$ has $n$ eigenvalues.

Proof:
Let $p_A$ be the characteristic polynomial of $\mathbf A$.
By definition, an eigenvalue of $\mathbf A$ is a root of $p_A$.
Since Degree of Characteristic Polynomial of Matrix equals Order of Matrix, the degree of $p_A$ is $n$.
From the Number of Roots of Polynomial With Complex Coefficients Equals Degree of Polynomial, $p_A$ has $n$ roots.
Therefore, $\mathbf A$ has $n$ eigenvalues.
{{qed}}
Theorem: Number of Linearly Independent Eigenvectors of Square Complex Matrix

Let $\mathbf A$ be a square matrix of order $n$ over the complex numbers $\C$.
Then $\mathbf A$ has no more than $n$ linearly independent eigenvectors.

Proof:
By the definition of eigenvalue, it is a root of the characteristic polynomial of $\mathbf A$.
By Degree of Characteristic Polynomial of Matrix equals Order of Matrix, the degree of the characteristic polynomial is $n$.
By Number of Roots of Polynomial With Complex Coefficients Equals Degree of Polynomial, the number of eigenvalues of $\mathbf A$, including multiplicity, is $n$.
Thus, the sum of the algebraic multiplicities of the distinct eigenvalues is $n$.
From Algebraic Multiplicity is not Less than Geometric Multiplicity, the sum of the geometric multiplicities of the distinct eigenvalues is no more than $n$.
Since geometric multiplicity is defined as the number of linearly independent eigenvectors associated with each distinct eigenvalue, the total number of linearly independent eigenvectors is no more than $n$.
{{qed}}
Theorem: Velocity from Integration of Equation of Motion

Let $P$ be a particle of constant mass $m$ moving under a force $\mathbf F$ as a function of time $t$ according to the '''equation of motion''':
:$m \dfrac {\d^2 \mathbf r} {\d t^2} = \map {\mathbf F} {\mathbf r}$
where $\mathbf r$ is the position vector of $P$.
Let the velocity of $P$ at time $t = 0$ be $\mathbf v_0$.
Then the velocity of $P$ at time $t$ is given by:
:$\mathbf v = \mathbf v_0 + \dfrac {\d \mathbf r} {\d t}$

Proof:
{{begin-eqn}}
{{eqn | l = m \dfrac {\d^2 \mathbf r} {\d t^2}
      | r = \map {\mathbf F} {\mathbf r}
      | c = 
}}
{{eqn | r = \dfrac {\map \d {m \mathbf v} } {\d t}
      | c = Newton's First Law of Motion
}}
{{eqn | ll= \leadsto
      | l = m \dfrac {\d^2 \mathbf r} {\d t^2}
      | r = m \dfrac {\d \mathbf v} {\d t}
      | c = {{hypothesis}}: mass $m$ is constant
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d^2 \mathbf r} {\d t^2}
      | r = \dfrac {\d \mathbf v} {\d t}
      | c = {{hypothesis}}: mass $m$ is constant
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d \mathbf r} {\d t}
      | r = \int_0^t \dfrac {\d \mathbf v} {\d t} \rd t
      | c = integrating both sides {{WRT|Integration}} $t$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d \mathbf r} {\d t}
      | r = \mathbf v - \mathbf v_0
      | c = Fundamental Theorem of Calculus
}}
{{end-eqn}}
{{qed}}
Theorem: Lattice Isomorphism is Isomorphism in Category Lat

Let $\mathbf{Lat}$ denote the category of lattices.
Let $f : L_1 \to L_2$ be a morphism of $\mathbf{Lat}$.
Then:
:$f$ is an isomorphism of $\mathbf{Lat}$ {{iff}} $f$ is a lattice isomorphsm

Proof:
Let $L_1$ and $L_2$ be the lattices $L_1 = \struct{A_1, \vee_1, \wedge_1, \preceq_1}$ and $L_2 = \struct{A_2, \vee_2, \wedge_2, \preceq_2}$ respectively.
By definition of category of lattices:
:$f$ is a lattice homomorphisms
By definition of an isomorphism:
:$f$ be an isomorphism of $\mathbf{Lat}$
{{iff}}:
:$(1):$ there exists a morphism of $g : L_2 \to L_1$ of $\mathbf{Lat}$ such that:
::$g \circ f = \operatorname{id}_{L_1}$ and $f \circ g = \operatorname{id}_{L_2}$
:where $\operatorname{id}_{L_1}$ and $\operatorname{id}_{L_2}$ are identity morphisms.
By definition of category of lattices:
:$f$ satisfies $(1)$
{{iff}}:
:$(2):$ there exists a lattice homomorphism $g : L_2 \to L_1$ such that:
::the standard compositions of mappings $g \circ f = \operatorname{id}_{A_1}$ and $f \circ g = \operatorname{id}_{A_2}$
:where $\operatorname{id}_{A_1}$ and $\operatorname{id}_{A_2}$ are identity mappings.
Theorem: Creation of Orthogonal Vector from Independent Vectors

Let $\mathbf V$ be a vector space.
Let $\mathbf a$ and $\mathbf b$ be vectors of $\mathbf V$ such that $\mathbf a$ and $\mathbf b$ form a linearly independent set.
Let $\mathbf a$ and $\mathbf b$ be expressed as column vectors.
Let $\mathbf b'$ be calculated as:
:$\mathbf b' = \mathbf b - \dfrac {\mathbf a^\intercal \mathbf b} {\mathbf a^\intercal \mathbf a} \mathbf a$
where $\mathbf a^\intercal$ denotes the transpose of $\mathbf a$.
Then $\mathbf b'$ is orthogonal to $\mathbf a$.

Proof:
{{Recall|Orthogonal (Linear Algebra)|orthogonal}}:
{{:Definition:Orthogonal (Linear Algebra)}}
We will show that $\mathbf b'^\intercal \mathbf a = 0$.
{{explain|why the inner product of $\mathbf a$ and $\mathbf b$ is the operation $\mathbf b'^\intercal \mathbf a$}}
{{begin-eqn}}
{{eqn | l = \mathbf b'^\intercal \mathbf a
      | r = \paren {\mathbf b - \dfrac {\mathbf a^\intercal \mathbf b} {\mathbf a^\intercal \mathbf a} \mathbf a}^\intercal \mathbf a
}}
{{eqn | r = \paren {\mathbf b^\intercal - \frac {\mathbf a^\intercal \mathbf b} {\mathbf a^\intercal \mathbf a} \mathbf a^\intercal} \mathbf a
}}
{{eqn | r = \mathbf b^\intercal \mathbf a - \frac {\mathbf a^\intercal \mathbf b} {\mathbf a^\intercal \mathbf a} \mathbf a^\intercal \mathbf a
}}
{{eqn | r = \mathbf b^\intercal \mathbf a - \mathbf a^\intercal \mathbf b
}}
{{eqn | r = \mathbf a^\intercal \mathbf b - \mathbf a^\intercal \mathbf b
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed}}
Theorem: Coset Space wrt Subring forms Ring iff Subring is Ideal

Let $\struct {R, +, \circ}$ be a ring.
Let $S$ be a subring of $R$.
For $a \in R$, let $\paren {a + S}$ denote the coset of $S$ by $a$.
Then:
:The coset space of $R$ {{WRT}} $S$ forms a ring
{{iff}}:
:$S$ is an ideal of $R$.

Proof:
{{ProofWanted|bit more consolidation of background needed yet}}
Theorem: Basis of Point Lattice is not Necessarily Unique

Let $\LL$ be a point lattice of dimension $n$.
Let $\BB = \set {\mathbf v_1, \mathbf v_2, \ldots, \mathbf v_n}$ be a basis of $\LL$.
Then it is not necessarily the case that $\BB$ is the '''only''' basis of $\LL$.

Proof:
{{MissingLinks}}
Let $\LL$ be a point lattice of dimension $n$.
Let $\BB = \set {\mathbf v_1,\mathbf v_2,\dots,\mathbf v_n}$ be a basis of $\LL$.
Let $\BB' = \set {\mathbf v_1, \mathbf v_1 + \mathbf v_2, \dots, \mathbf v_n} = \set {\mathbf w_1, \mathbf w_2, \dots, \mathbf w_n}$.
We will show that $\BB'$ is a basis for $\LL$.
Theorem: Packing of Circles into Plane

The most space-efficient way to pack unit circles into the plane is to place their centers at the lattice points of the point lattice in $\R^n$ with a basis $\set {\tuple {2, 0}, \tuple {1, \sqrt 3} }$.

Proof:
{{ProofWanted|see Point Lattice/Examples/2-Dimensional}}
Theorem: Inverse of Frame Isomorphism is Frame Isomorphism

Let $L_1 = \struct {S_1, \preceq_1}$ and $L_2 = \struct {S_2, \preceq_2}$ be frames.
Let $\phi: L_1 \to L_2$ be a frame isomorphism.
Let $\phi^{-1} : S_2 \to S_1$ be the inverse of $\phi : S_1 \to S_2$.
Then:
:$\phi^{-1} : L_2 \to L_1$ is a frame isomorphism

Proof:
By definition of frame isomorphism:
:$\phi: L_1 \to L_2$ is a complete lattice isomorphism
From Inverse of Complete Lattice Isomorphism is Complete Lattice Isomorphism:
:$\phi^{-1} : L_2 \to L_1$ is a complete lattice isomorphism
By definition of frame isomorphism:
:$\phi^{-1}: L_2 \to L_1$ is a frame isomorphism
{{qed}}
Category:Frame Isomorphisms
7d4nwjmp1hch5d4froy09c3435gqbr6
Theorem: Inverse of Lattice Isomorphism is Lattice Isomorphism

Let $L_1 = \struct {A_1, \vee_1, \wedge_1, \preceq_1}$ and $L_2 = \struct {A_2, \vee_2, \wedge_2, \preceq_2}$ be lattices.
Let $\phi: L_1 \to L_2$ be a lattice isomorphism.
Let $\phi^{-1} : A_2 \to A_1$ be the inverse of $\phi : A_1 \to A_2$.
Then:
:$\phi^{-1} : L_2 \to L_1$ is a lattice isomorphism

Proof:
By definition, a lattice isomorphism is a bijective lattice homomorphism.
The result follows from Inverse of Bijective Lattice Homomorphism is Bijective Lattice Homomorphism.
{{qed}}
Category:Lattice Isomorphisms
i95oqn5vwwxq6ea85bsheaycwjh75sh
Theorem: Frame Homomorphism is Lattice Homomorphism

Let $L_1 = \struct{S_1, \preceq_1}$ and $L_2 = \struct{S_2, \preceq_2}$ be frames.
Let $\phi: L_1 \to L_2$ be a frame homomorphism.
Then:
:$\phi: \struct{S_1, \vee_1, \wedge_1, \preceq_1} \to \struct{S_2, \vee_2, \wedge_2, \preceq_2}$ is a lattice homomorphism
where:
:$\wedge_1, \vee_1$ denote  the meet and join on $L_1$
:$\wedge_2, \vee_2$ denote  the meet and join on $L_2$

Proof:
By definition of frame:
:$L_1$ and $L_2$ are complete lattices
From Complete Lattice is Lattice:
:$\struct{S_1, \vee_1, \wedge_1, \preceq_1}$ and $\struct{S_2, \vee_2, \wedge_2, \preceq_2}$ are lattices
where:
:$\wedge_1, \vee_1$ denote  the meet and join on $L_1$
:$\wedge_2, \vee_2$ denote  the meet and join on $L_2$
By definition of frame homomorphism:
:$\phi$ is arbitrary join preserving and finite meet preserving
That is $\phi$ satifies:
:$\forall A \subseteq S_1 : \map \phi {\sup A} = \sup \set{\map \phi a : a \in A}$
:$\forall$ finite $A \subseteq S_1 : \map \phi {\inf A} = \inf \set{\map \phi a : a \in A}$
Hence $\phi$ satisfies:
:$\forall$ $a, b \in S_1 : \map \phi {a \wedge_1 b} = \map \phi a \wedge_2 \map \phi b$
:$\forall$ $a, b \in S_1 : \map \phi {a \vee_1 b} = \map \phi a \vee_2 \map \phi b$
by definition of meet and join
By definition of the morphism property:
:$\vee_1, \wedge_1$ have the morphism property under $\phi$
Hence $\phi$ is a lattice homomorphism by definition.
{{qed}}
Category:Frame Homomorphisms
Category:Lattice Homomorphisms
boo746yrjy5klole0b14jqgcioedzg0
Theorem: Ramanujan's Continued Fraction of One

Let $x \notin \Z_{<0}$.
Then: 
:$1 = \cfrac {x + 1} {x + \cfrac {x + 2} {x + 1 + \cfrac {x + 3 } {x + 2 + \ddots} } }$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = 1
      | r = \frac {x + 1} {x + 1}
      | c = 
}}
{{eqn | r = \cfrac {x + 1} {x + \cfrac {x + 2} {x + 2} }
      | c = 
}}
{{eqn | r = \cfrac {x + 1} {x + \cfrac {x + 2} {x + 1 + 1} }
      | c = 
}}
{{eqn | r = \cfrac {x + 1} {x + \cfrac {x + 2} {x + 1 + \cfrac {x + 3} {x + 3} } }
      | c = 
}}
{{eqn | r = \cfrac {x + 1} {x + \cfrac {x + 2} {x + 1 + \cfrac {x + 3} {x + 2 + 1} } }
      | c = 
}}
{{end-eqn}}
In order for this sequence to continue, it needs to be shown that:
:$x + n = x + \paren {n - 1} + \dfrac {x + n + 1} {x + n + 1}$
Thus:
{{begin-eqn}}
{{eqn | l = x + n
      | r = x + n - 1 + 1
      | c = 
}}
{{eqn | r = x + n - 1 + \frac {x + n + 1} {x + n + 1}
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
{{Namedfor|Srinivasa Ramanujan|cat = Ramanujan}}
Theorem: Continued Fraction for Real Arctangent Function

:$\arctan x = \cfrac x {1 + \cfrac {x^2} {3 - x^2 + \cfrac {\paren {3 x}^2} {5 - 3 x^2 + \cfrac {\paren {5 x}^2} {7 - 5 x^2 + \cfrac {\paren {7 x}^2} {\ddots } } } } }$

Proof:
{{begin-eqn}}
{{eqn | l = \arctan x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {2 n + 1}
      | c = Power Series Expansion for Real Arctangent Function for $-1 \le x \le 1$
}}
{{eqn | r = x - \dfrac {x^3} 3 + \dfrac {x^5} 5 - \dfrac {x^7} 7 + \cdots
      | c = 
}}
{{eqn | r = x + x \paren {\dfrac {-x^2} 3} + x \paren {\dfrac {-x^2} 3} \paren {\dfrac {-3 x^2} 5} + x \paren {\dfrac {-x^2} 3} \paren {\dfrac {-3 x^2} 5} \paren {\dfrac {-5 x^2} 7} + \cdots
      | c = 
}}
{{eqn | r = a_0 + a_0 a_1 + a_0 a_1 a_2 + a_0 a_1 a_2 a_3 + \cdots
      | c =
}}
{{end-eqn}}
From Euler's Continued Fraction Formula, we have:
:$a_0 + a_0 a_1 + a_0 a_1 a_2 + a_0 a_1 a_2 a_3 + \cdots = \cfrac {a_0} {1 - \cfrac {a_1} {1 + a_1 - \cfrac {a_2} {1 + a_2 - \cfrac {a_3} {1 + a_3 - \cfrac {\ddots} {\ddots  } } } } }$
Therefore:
{{begin-eqn}}
{{eqn | l = x + x \paren {\dfrac {-x^2} 3} + x \paren {\dfrac {-x^2} 3} \paren {\dfrac {-3 x^2} 5} + x \paren {\dfrac {-x^2} 3} \paren {\dfrac {-3 x^2} 5} \paren {\dfrac {-5 x^2} 7} + \cdots
      | r = \cfrac x {1 - \cfrac {\paren {\dfrac {-x^2} 3} } {1 + \paren {\dfrac {-x^2} 3} - \cfrac {\paren {\dfrac {-3 x^2} 5} } {1 + \paren {\dfrac {-3 x^2} 5} - \cfrac {\paren {\dfrac {-5 x^2} 7} } {1 + \paren {\dfrac {-5 x^2} 7} - \cfrac {\ddots} {\ddots  } } } } }
      | c = 
}}
{{eqn | r = \cfrac x {1 - \cfrac {\paren {\dfrac {-x^2} 3} \times 3 } {3 \times \paren {1 + \paren {\dfrac {-x^2} 3} } - \cfrac {\paren {\dfrac {-3 x^2} 5} \times 3 \times 5 } {5 \times \paren {1 + \paren {\dfrac {-3 x^2} 5} } - \cfrac {\paren {\dfrac {-5 x^2} 7} \times 5 \times 7 } {7 \times \paren {1 + \paren {\dfrac {-5 x^2} 7} } - \cfrac {\ddots} {\ddots  } } } } }
      | c = multiplying by $1$
}}
{{eqn | r = \cfrac x {1 + \cfrac {x^2} {3 - x^2 + \cfrac {\paren {3 x}^2} {5 - 3 x^2 + \cfrac {\paren {5 x}^2} {7 - 5 x^2 + \cfrac {\paren {7 x}^2} {\ddots } } } } }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Probability Mass Function of Negative Binomial Distribution (Type 2)/Also defined as

Let $X$ be a discrete random variable on a probability space $\struct {\Omega, \Sigma, \Pr}$.
Let $X$ have the '''type $2$ negative binomial distribution with parameters $r$ and $p$''', defined as the number of failures before $r$ successes have occurred.
Then the probability mass function of $X$ is given by:
:$\map \Pr {X = k} = \dbinom {k + r - 1} {r - 1} p^r \paren {1 - p}^k$
where:
:$\Img X = \set {0, 1, 2, \ldots}$
:$0 < p < 1$.

Proof:
{{Recall|Negative Binomial Distribution (Type 2)|subdef = Also defined as}}
{{:Definition:Negative Binomial Distribution (Type 2)/Also defined as}}
The number of Bernoulli trials may be as few as $0$, so the image is correct:
:$\Img X = \set {0, 1, 2, \ldots}$
If $X$ takes the value $k$, then there must have been $k + r$ trials altogether.
So, after $r + k - 1$ trials, there must have been $r - 1$ successes, as (from the description of the experiment) the last trial is a success.
So the probability of the occurrence of the event $\sqbrk {X = k}$ is given by the binomial distribution, as follows:
:$\map {p_X} k = \dbinom {k + r - 1} {r - 1} p^r \paren {1 - p}^k$
where $k \in \set {0, 1, 2, \ldots}$
Hence the result, by definition of probability mass function.
{{qed}}