avewright/proofwiki-math huggingface dataset:
Theorem: Meet-Continuous iff Ideal Supremum is Meet Preserving

Let $\mathscr S = \struct {S, \vee, \wedge, \preceq}$ be an up-complete lattice.
Let $f: \map {\it Ids} {\mathscr S} \to S$ be a mapping such that:
:$\forall I \in \map {\it Ids} {\mathscr S}: \map f I = \sup_{\mathscr S} I$
where 
:$\map {\it Ids} {\mathscr S}$ denotes the set of all ideals in $\mathscr S$
Then
:$\mathscr S$ is meet-continuous
{{iff}}
:$f$ preserves meet as a mapping from $\struct {\map {\it Ids} {\mathscr S}, \subseteq}$ into $\mathscr S$

Proof:
=== Sufficient Condition ===
Let $\mathscr S$ be meet-continuous.
We will prove that:
:for every directed subsets $D_1, D_2$ of $S$: $\paren {\sup D_1} \wedge \paren {\sup D_2} = \sup \set {d_1 \wedge d_2: d_1 \in D_1, d_2 \in D_2}$
Let $D_1, D_2$ be directed subsets of $S$.
we will prove as sublemma that:
:for every an element $x$ of $S$, a directed subset $D$ of $S$ if $x \preceq \sup D$, then $x = \sup \set {x \wedge d: d \in D}$
Let $x \in S$, $D$ be a directed subset of $S$ such that:
:$x \preceq \sup D$
Thus:
{{begin-eqn}}
{{eqn | l = x
      | r = x \wedge \sup D
      | c = Preceding iff Meet equals Less Operand
}}
{{eqn | r = \sup \set {x \wedge d: d \in D}
      | c = {{Defof|Meet-Continuous Lattice}}
}}
{{end-eqn}}
By definition of reflexivity:
:for every element $x$ of $S$, a directed subset $D$ of $S$ if $x \preceq \sup D$, then $x \preceq \sup \set {x \wedge d: d \in D}$
Define a mapping $g: S \times S \to S$:
:$\forall \tuple {s, t} \in S \times S: \map g {s, t} = s \wedge t$
By Meet is Directed Suprema Preserving:
:$g$ preserves directed suprema as a mapping from the simple order product $\struct {S \times S, \precsim}$ of $\mathscr S$ and $\mathscr S$ into $\mathscr S$.
Thus by Meet is Directed Suprema Preserving implies Meet of Suprema equals Supremum of Meet of Directed Subsets: 
:$\paren {\sup D_1} \wedge \paren {\sup D_2} = \sup \set {d_1 \wedge d_2: d_1 \in D_1, d_2 \in D_2}$
By exemplification:
:for every ideals $I_1, I_2$ of $S$: $\paren {\sup I_1} \wedge \paren {\sup I_2} = \sup \set {d_1 \wedge d_2: d_1 \in I_1, d_2 \in I_2}$
Thus by Meet of Suprema equals Supremum of Meet of Ideals implies Ideal Supremum is Meet Preserving:
:$f$ preserves meet.
{{qed|lemma}}
Theorem: Rational Number is Algebraic

Let $r \in \Q$ be a rational number.
Then $r$ is also an algebraic number.

Proof:
Let $r$ be expressed in the form:
:$r = \dfrac p q$
Consider the linear function in $x$:
:$q x - p = 0$
which has the solution:
:$x = \dfrac p q$
Hence the result, by definition of algebraic number.
{{qed}}
Theorem: Rational Number is Algebraic of Degree 1

Let $r \in \Q$ be a rational number.
Then $r$ is an algebraic number of degree $1$.

Proof:
Let $r$ be expressed in the form:
:$r = \dfrac p q$
By Rational Number is Algebraic, $r$ can be expressed as the root of the linear function:
:$q x - p = 0$
A polynomial of degree zero is a constant polynomial, and has no roots.
Hence the result by definition of degree of algebraic number.
{{qed}}
Theorem: Square Root of 2 is Algebraic of Degree 2

The square root of $2$ is an algebraic number of degree $2$.

Proof:
Suppose $\sqrt 2$ could be expressed as the root of the linear function:
:$a_1 x + a_0 = 0$
for some $a_0, a_1 \in \Q$.
Then:
:$\sqrt 2 = -\dfrac {a_0} {a_1}$
and would be rational.
But as Square Root of 2 is Irrational, this is not the case.
However, $\sqrt 2$ is a root of the polynomial of degree $2$:
:$x^2 - 2 = 0$
Hence the result by definition of degree of algebraic number.
{{qed}}
Theorem: Gelfond-Schneider Constant is Transcendental

The Gelfond-Schneider constant:
:$2^{\sqrt 2}$
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.
From Rational Number is Algebraic:
:$2$ is algebraic.
From Square Root of 2 is Algebraic of Degree 2:
:$\sqrt 2$ is algebraic.
From Square Root of 2 is Irrational:
:$\sqrt 2$ is irrational.
Hence the result.
{{qed}}
Theorem: Bernoulli Numbers are Rational

The Bernoulli numbers are rational.

Proof:
By the recurrence relation for the Bernoulli numbers:
:$B_n = \begin{cases} 1 & : n = 0 \\
\ds - \sum_{k \mathop = 0}^{n-1} \binom n k \frac {B_k} {n - k + 1} & : n > 0
\end{cases}$
:$B_0$ is rational.
:$B_n$ is a finite sum of the products of a binomial coefficient with a Bernoulli number earlier in the sequence divided by an integer.
The proof proceeds by induction.
For all $n \in \N$, let $\map P n$ be the proposition:
:$B_n$ is rational.
Theorem: Power Series Expansion for Tangent Function/Proof of Convergence

The radius of convergence of the Power Series Expansion for Tangent Function:
:$\ds \tan x = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} } {\paren {2 n}!} x^{2 n - 1}$
where $B_{2 n}$ denotes the Bernoulli numbers, is given as:
:$\size x < \dfrac \pi 2$

Proof:
By Combination Theorem for Limits of Real Functions we can deduce the following.
{{begin-eqn}}
{{eqn | o = 
      | r = \lim_{n \mathop \to \infty} \size {\frac {\frac {\paren {-1}^n 2^{2 n + 2} \paren {2^{2 n + 2} - 1} B_{2 n + 2} } {\paren {2 n + 2}!} x^{2 n + 1} } {\frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} } {\paren {2 n}!} x^{2 n - 1} } }
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\frac {\paren {2^{2 n + 2} - 1} } {\paren {2^{2 n} - 1} } \frac 1 {\paren {2 n + 1} \paren {2 n + 2} } \frac {B_{2 n + 2} } {B_{2 n} } } 4 x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\frac {2^{2 n + 2} - 1} {2^{2 n} - 1} } \size {\frac 1 {\paren {2 n + 1} \paren {n + 1} } \frac {B_{2 n + 2} } {B_{2 n} } } 2 x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {4 \frac {2^{2 n} } {2^{2 n} - 1} - \frac 1 {2^{2 n} - 1} } \size {\frac 1 {\paren {2 n + 1} \paren {n + 1} } \frac {B_{2 n + 2} } {B_{2 n} } } 2 x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {4 + \frac 4 {2^{2 n} - 1} - \frac 1 {2^{2 n} - 1} } \size {\frac 1 {\paren {2 n + 1} \paren {n + 1} } \frac {B_{2 n + 2} } {B_{2 n} } } 2 x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\frac 1 {\paren {2 n + 1} \paren {n + 1} } \frac {B_{2 n + 2} } { B_{2 n} } } 8 x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\frac 1 {\paren {2 n + 1} \paren {n + 1} } \frac {\paren {-1}^{n + 2} 4 \sqrt {\pi \paren {n + 1} } \paren {\frac {n + 1} {\pi e} }^{2 n + 2} } {\paren {-1}^{n + 1} 4 \sqrt {\pi n} \paren {\frac n {\pi e} }^{2 n} } } 8 x^2
      | c = Asymptotic Formula for Bernoulli Numbers
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\frac {\paren {n + 1}^2} {\paren {2 n + 1} \paren {n + 1} } \sqrt {\frac {n + 1} n } \paren {\frac {n + 1} n}^{2 n} } \frac 8 {\pi^2 e^2} x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\paren {\frac {n + 1} n}^{2 n} } \frac 4 {\pi^2 e^2} x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\paren {\paren {1 + \frac 1 n}^n}^2} \frac 4 {\pi^2 e^2} x^2
      | c =
}}
{{eqn | r = \frac {4 e^2} {\pi^2 e^2} x^2
      | c = {{Defof|Euler's Number as Limit of Sequence}}
}}
{{eqn | r = \frac 4 {\pi^2} x^2
      | c =
}}
{{end-eqn}}
This is less than $1$ {{iff}}:
:$\size x < \dfrac \pi 2$
Hence by the Ratio Test, the series converges for $\size x < \dfrac \pi 2$.
Theorem: Power Series Expansion for Tangent Function/Sequence

The Power Series Expansion for Tangent Function begins:
:$\tan x = x + \dfrac 1 3 x^3 + \dfrac 2 {15} x^5 + \dfrac {17} {315} x^7 + \dfrac {62} {2835} x^9 + \cdots$

Proof:
From Power Series Expansion for Tangent Function:
{{begin-eqn}}
{{eqn | l = \tan x
      | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} } {\paren {2 n}!} x^{2 n - 1}
      | c = 
}}
{{eqn | r = \frac {2^2 \paren {2^2 - 1} B_2} {2!} x - \frac {2^4 \paren {2^4 - 1} B_4} {4!} x^3 + \frac {2^6 \paren {2^6 - 1} B_6} {6!} x^5 - \frac {2^8 \paren {2^8 - 1} B_8} {8!} x^7 + \frac {2^{10} \paren {2^{10} - 1} B_{10} } {10!} x^9 - \cdots
      | c = 
}}
{{end-eqn}}
Enumerating the Bernoulli numbers:
{{begin-eqn}}
{{eqn | l = B_2
      | r = \dfrac 1 6
}}
{{eqn | l = B_4
      | r = -\dfrac 1 {30}
}}
{{eqn | l = B_6
      | r = \dfrac 1 {42}
}}
{{eqn | l = B_8
      | r = -\dfrac 1 {30}
}}
{{eqn | l = B_{10}
      | r = \dfrac 5 {66}
}}
{{end-eqn}}
Thus the appropriate arithmetic is performed on each coefficient:
{{begin-eqn}}
{{eqn | l = \frac {2^2 \paren {2^2 - 1} B_2} {2!}
      | r = \frac {4 \times 3} {2} \times \dfrac 1 6
}}
{{eqn | r = 1
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = -\frac {2^4 \paren {2^4 - 1} B_4} {4!}
      | r = -\dfrac {16 \times 15} {24} \times \dfrac {-1} {30}
}}
{{eqn | r = \dfrac {\paren {2^4} \times \paren {3 \times 5} } {\paren {2^3 \times 3} \times \paren {2 \times 3 \times 5} }
}}
{{eqn | r = \dfrac 1 3
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \frac {2^6 \paren {2^6 - 1} B_6} {6!}
      | r = \dfrac {64 \times 63} {720} \times \dfrac 1 {42}
}}
{{eqn | r = \dfrac {\paren {2^6} \times \paren {3^2 \times 7} } {\paren {2^4 \times 3^2 \times 5} \times \paren {2 \times 3 \times 7} }
}}
{{eqn | r = \dfrac 2 {15}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = -\frac {2^8 \paren {2^8 - 1} B_8} {8!}
      | r = -\dfrac {256 \times 255} {40 \, 320} \times \dfrac {-1} {30}
}}
{{eqn | r = \dfrac {\paren {2^8} \times \paren {3 \times 5 \times 17} } {\paren {2^7 \times 3^2 \times 5 \times 7} \times \paren {2 \times 3 \times 5} }
}}
{{eqn | r = \dfrac {17} {3^2 \times 5 \times 7}
}}
{{eqn | r = \dfrac {17} {315}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \frac {2^{10} \paren {2^{10} - 1} B_{10} } {10!}
      | r = \dfrac {1024 \times 1023} {3 \, 628 \, 800} \times \dfrac 5 {66}
}}
{{eqn | r = \dfrac {\paren {2^{10} } \times \paren {3 \times 11 \times 31} \times 5} {\paren {2^8 \times 3^4 \times 5^2 \times 7} \times \paren {2 \times 3 \times 11} }
}}
{{eqn | r = \dfrac {2 \times 31} {\paren {3^4 \times 5 \times 7} }
}}
{{eqn | r = \dfrac {62} {2835}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Tangent to Cycloid is Vertical at Cusps

The tangent to the cycloid whose locus is given by:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
is vertical at the cusps.

Proof:
From Slope of Tangent to Cycloid, the slope of the tangent to $C$ at the point $\tuple {x, y}$ is given by:
:$\dfrac {\d y} {\d x} = \cot \dfrac \theta 2$
At the cusps, $\theta = 2 n \pi$ for $n \in \Z$.
Thus at the cusps, the slope of the tangent to $C$ is $\cot n \pi$.
From Shape of Cotangent Function:
:$\ds \lim_{\theta \mathop \to n \pi} \cot \theta \to \infty$
Hence the result by definition of vertical tangent line.
{{qed}}
Theorem: Tangent to Cycloid passes through Top of Generating Circle

Let $C$ be a cycloid generated by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
Then the tangent to $C$ at a point $P$ on $C$ passes through the top of the generating circle of $C$.

Proof:
From Tangent to Cycloid, the equation for the tangent to $C$ at a point $P = \tuple {x, y}$ is given by:
:$(1): \quad y - a \paren {1 - \cos \theta} = \dfrac {\sin \theta} {1 - \cos \theta} \paren {x - a \theta + a \sin \theta}$
From Equation of Cycloid, the point at the top of the generating circle of $C$ has coordinates $\tuple {2 a, a \theta}$.
Substituting $x = 2 a$ in $(1)$:
{{begin-eqn}}
{{eqn | l = y - a \paren {1 - \cos \theta}
      | r = \dfrac {\sin \theta} {1 - \cos \theta} \paren {a \theta - a \theta + a \sin \theta}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = a \paren {1 - \cos \theta} + \dfrac {\sin \theta} {1 - \cos \theta} a \sin \theta
      | c = 
}}
{{eqn | r = \frac {a \paren {1 - \cos \theta}^2 + a \sin^2 \theta} {1 - \cos \theta}
      | c = 
}}
{{eqn | r = \frac {a \paren {1 - 2 \cos \theta + \cos^2 \theta} + a \sin^2 \theta} {1 - \cos \theta}
      | c = 
}}
{{eqn | r = \frac {a \paren {1 - 2 \cos \theta + 1} } {1 - \cos \theta}
      | c = 
}}
{{eqn | r = \frac {a \paren {2 - 2 \cos \theta} } {1 - \cos \theta}
      | c = 
}}
{{eqn | r = 2 a
      | c = 
}}
{{end-eqn}}
That is, the tangent to $C$ passes through $\tuple {a \theta, 2 a}$ as was required.
{{qed}}
Theorem: Tangent to Cycloid

Let $C$ be a cycloid generated by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
Then the tangent to $C$ at a point $\tuple {x, y}$ on $C$ is given by the equation:
:$y - a \paren {1 - \cos \theta} = \dfrac {\sin \theta} {1 - \cos \theta} \paren {x - a \theta + a \sin \theta}$

Proof:
By Derivative of Curve at Point, the tangent to $C$ at the point $\tuple {x, y}$ is the derivative of its equation at that point.
Thus:
{{begin-eqn}}
{{eqn | l = \frac {\d x} {\d \theta}
      | r = a \paren {1 - \cos \theta}
      | c = 
}}
{{eqn | l = \frac {\d y} {\d \theta}
      | r = a \sin \theta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac {\d y} {\d \theta} / \frac {\d x} {\d \theta}
      | c = 
}}
{{eqn | r = \frac {a \sin \theta} {a \paren {1 - \cos \theta} }
      | c = 
}}
{{eqn | r = \frac {\sin \theta} {1 - \cos \theta}
      | c = 
}}
{{eqn | r = \frac 1 {\map \tan {\theta / 2} }
      | c = {{Corollary|Half Angle Formula for Tangent|2}}
}}
{{eqn | r = \cot \frac \theta 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Tangent to Cycloid

Let $C$ be a cycloid generated by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
Then the tangent to $C$ at a point $\tuple {x, y}$ on $C$ is given by the equation:
:$y - a \paren {1 - \cos \theta} = \dfrac {\sin \theta} {1 - \cos \theta} \paren {x - a \theta + a \sin \theta}$

Proof:
Consider a polygon $ABCD$ being rolled along a straight line in the same way as the generating circle of $C$.
Let $A', B', C', D'$ be the points around which the $ABCD$ rotates while rolling.
:600px
The point $A$ traces out in succession several arcs of circles with centers $B', C', D'$.
The tangent to each of these arcs is perpendicular to the line joining the point of tangency to the corresponding point of rotation.
Consider a circle as being a polygon with an infinite number of sides.
It follows that in the limit the tangent to $C$ at any given point is perpendicular to the line joining the point of tangency to the corresponding point where the generating circle touches the straight line along which the generating circle rolls.
:600px
Let $O$ be the center of the generating circle.
Let $P$ be the point of tangency.
Let $Q$ be the point where the generating circle touches the straight line along which the generating circle rolls.
Let $S$ be the point where the tangent to $C$ meets the straight line along which the generating circle rolls.
As $OP$ and $OQ$ are both radii of the generating circle:
:$OP = OQ = a$
and so $\triangle POQ$ is isosceles.
Let $R$ be dropped perpendicular to $PQ$ at $R$.
As $\triangle POQ$ is isosceles, $\triangle OPR = \triangle OQR$ and so $PR = RQ$.
Thus $\angle POR = \angle QOR = \dfrac \theta 2$.
As $OR \perp PR$ and $PR \perp PS$, we have that $\triangle OPR$ is similar to $\triangle QPS$.
Thus $\angle PQS = \angle POR$ and so $\angle PSQ$ is $\dfrac \pi 2 - \angle POR = \dfrac \pi 2 - \dfrac \theta 2$.
By definition, $\tan \angle PSQ$ is the slope of the tangent $\dfrac {\d y} {\d x}$ to $C$.
Thus:
{{begin-eqn}}
{{eqn | l = \dfrac {\d y} {\d x}
      | r = \tan \angle PSQ
      | c = 
}}
{{eqn | r = \map \tan {\dfrac \pi 2 - \dfrac \theta 2}
      | c = 
}}
{{eqn | r = \cot \frac \theta 2
      | c = Tangent of Complement equals Cotangent
}}
{{end-eqn}}
{{qed}}
Theorem: Tangent to Cycloid

Let $C$ be a cycloid generated by the equations:
:$x = a \paren {\theta - \sin \theta}$
:$y = a \paren {1 - \cos \theta}$
Then the tangent to $C$ at a point $\tuple {x, y}$ on $C$ is given by the equation:
:$y - a \paren {1 - \cos \theta} = \dfrac {\sin \theta} {1 - \cos \theta} \paren {x - a \theta + a \sin \theta}$

Proof:
From Slope of Tangent to Cycloid, the slope of the tangent to $C$ at the point $\tuple {x, y}$ is given by:
:$\dfrac {\d y} {\d x} = \cot \dfrac \theta 2$
This tangent to $C$ also passes through the point $\tuple {a \paren {\theta - \sin \theta},  a \paren {1 - \cos \theta} }$.
We have:
{{begin-eqn}}
{{eqn | l = \tan \dfrac \theta 2
      | r = \dfrac {1 - \cos \theta} {\sin \theta}
      | c = {{Corollary|Half Angle Formula for Tangent|2}}
}}
{{eqn | ll= \leadsto
      | l = \cot \dfrac \theta 2
      | r = \dfrac {\sin \theta} {1 - \cos \theta}
      | c = Cotangent is Reciprocal of Tangent
}}
{{end-eqn}}
By Equation of Straight Line in Plane we have:
:$y - y_0 = m \paren {x - x_0}$
where $m$ is the slope and $\tuple {x_0, y_0}$ a given point on the straight line.
Substituting for the slope $m$ we obtain:
:$y - y_0 = \dfrac {\sin \theta} {1 - \cos \theta} \paren {x - x_0}$
Substituting for the given point $\tuple {a \paren {\theta - \sin \theta},  a \paren {1 - \cos \theta} }$
:$y - a \paren {1 - \cos \theta} = \dfrac {\sin \theta} {1 - \cos \theta} \paren {x - a \paren {\theta - \sin \theta} }$
Hence the result.
{{qed}}
Theorem: Equation of Hypocycloid

Let a circle $C_1$ of radius $b$ roll without slipping around the inside of a circle $C_2$ of (larger) radius $a$.
Let $C_2$ be embedded in a cartesian plane with its center $O$ located at the origin.
Let $P$ be a point on the circumference of $C_1$.
Let $C_1$ be initially positioned so that $P$ is its point of tangency to $C_2$, located at point $A = \tuple {a, 0}$ on the $x$-axis.
Let $H$ be the hypocycloid traced out by the point $P$.
Let $\tuple {x, y}$ be the coordinates of $P$ as it travels over the plane.
The point $P = \tuple {x, y}$ is described by the equations:
:$x = \paren {a - b} \cos \theta + b \map \cos {\paren {\dfrac {a - b} b} \theta}$
:$y = \paren {a - b} \sin \theta - b \map \sin {\paren {\dfrac {a - b} b} \theta}$

Proof:
:500px
Let $C_1$ have rolled so that the line $OB$ through the radii of $C_1$ and $C_2$ is at angle $\theta$ to the $x$-axis.
Let $C_1$ have turned through an angle $\phi$ to reach that point.
By definition of sine and cosine, $P = \tuple {x, y}$ is defined by:
:$x = \paren {a - b} \cos \theta + b \map \cos {\phi - \theta}$
:$y = \paren {a - b} \sin \theta - b \map \sin {\phi - \theta}$
The arc of $C_1$ between $P$ and $B$ is the same as the arc of $C_2$ between $A$ and $B$.
Thus by Arc Length of Sector:
:$ a \theta = b \phi$
Thus:
:$\phi - \theta = \paren {\dfrac {a - b} b} \theta$
whence the result.
{{qed}}
Theorem: Meet in Set of Ideals

Let $\mathscr S = \struct {S, \preceq}$ be a meet semilattice.
Let $\map {\it Ids} {\mathscr S}$ be the set of all ideals in $\mathscr S$.
Let $I_1, I_2$ be ideals in $\mathscr S$.
Then
:$I_1 \wedge I_2 = \set {i_1 \wedge i_2: i_1 \in I_1, i_2 \in I_2}$
where
:$I_1 \wedge I_2$ denotes the meet in $\struct {\map {\it Ids} {\mathscr S}, \subseteq}$

Proof:
By Meet is Intersection in Set of Ideals:
:$I_1 \wedge I_2 = I_1 \cap I_2$
Theorem: Intersection of Semilattice Ideals is Ideal

Let $\struct {S, \preceq}$ be a meet semilattice.
Let $I_1, I_2$ be ideals in $\struct {S, \preceq}$.
Then $I_1 \cap I_2$ is ideal in $\struct {S, \preceq}$

Proof:
=== Directed Subset ===
Let $x, y \in I_1 \cap I_2$.
By definition of intersection:
:$x, y \in I_1$ and $x, y \in I_2$
By definition of directed subset:
:$\exists z_1 \in I_1: x \preceq z_1 \land y \preceq z_1$
and
:$\exists z_2 \in I_2: x \preceq z_2 \land y \preceq z_2$
By Meet Precedes Operands:
:$z_1 \wedge z_2 \preceq z_1$ and $z_1 \wedge z_2 \preceq z_2$
By definition of lower section:
:$z_1 \wedge z_2 \in I_1$ and $z_1 \wedge z_2 \in I_2$
By definition of intersection:
:$z_1 \wedge z_2 \in I_1 \cap I_2$
By definition of meet:
:$z_1 \wedge z_2 = \inf \set {z_1, z_2}$
By definition of infimum:
:$x \preceq z_1 \wedge z_2$ and $y \preceq z_1 \wedge z_2$
Thus by definition:
:$I_1 \cap I_2$ is directed.
{{qed|lemma}}
Theorem: Number of Cusps of Hypocycloid from Integral Ratio of Circle Radii

Let $H$ be a hypocycloid $H$ generated by a circle $C_1$ of radius $b$ rolling within a circle $C_2$ of (larger) radius $a$.
Let $a = n b$ where $n$ is an integer.
Then $H$ has $n$ cusps.

Proof:
The length of the arc of $C_2$ between two adjacent cusps of $H$ is $2 \pi b$.
The total length of the circumference of $C_1$ is $2 \pi a$.
Thus the total number of cusps of $H$ is:
:$\dfrac {2 \pi a} {2 \pi b} = \dfrac {2 \pi n b} {2 \pi b} = n$
{{qed}}
Theorem: Length of Tangent to Astroid between Axes equals Radius of Stator

Let $C_1$ be a circle of radius $b$ roll without slipping around the inside of a circle $C_2$ of radius $a = 4 b$.
Let $C_2$ be embedded in a cartesian plane with its center $O$ located at the origin.
Let $P$ be a point on the circumference of $C_1$.
Let $C_1$ be initially positioned so that $P$ is its point of tangency to $C_2$, located at point $A = \tuple {a, 0}$ on the $x$-axis.
Let $H$ be the astroid formed by the locus of $P$.
The segment of the tangent to $H$ between the $x$-axis and the $y$-axis is constant and equals the radius of the stator $C_2$.

Proof:
:400px
From Equation of Astroid, $H$ can be expressed as:
:$\begin {cases} x & = a \cos^3 \theta \\ y & = a \sin^3 \theta \end {cases}$
Thus the slope of the tangent to $H$ at $\tuple {x, y}$ is:
{{begin-eqn}}
{{eqn | l = \frac {\d y} {\d x}
      | r = \frac {3 a \sin^2 \theta \cos \theta \rd \theta} {-3 a \cos^2 \theta \sin \theta \rd \theta}
      | c = 
}}
{{eqn | r = -\tan \theta
      | c = 
}}
{{end-eqn}}
Thus the equation of the tangent to $H$ is given by:
:$y - a \sin^3 \theta = -\tan \theta \paren {x - a \cos^3 \theta}$
{{explain|Find, or post up, the equation of a line of given tangent passing through point $\tuple {x, y}$ as this is what is needed here}}
The $x$-intercept is found by setting $y = 0$ and solving for $x$:
{{begin-eqn}}
{{eqn | l = x
      | r = a \cos^3 \theta + a \sin^2 \theta \cos \theta
      | c = 
}}
{{eqn | r = a \cos \theta \paren {\cos^2 \theta + \sin^2 \theta}
      | c = 
}}
{{eqn | r = a \cos \theta
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
Similarly, the $y$-intercept is found by setting $x = 0$ and solving for $y$, which gives:
:$y = a \sin \theta$
The length of the part of the tangent to $H$ between the $x$-axis and the $y$-axis is given by:
{{begin-eqn}}
{{eqn | l = \sqrt {a^2 \cos^2 \theta + a^2 \sin^2 \theta}
      | r = a \sqrt {\cos^2 \theta + \sin^2 \theta}
      | c = 
}}
{{eqn | r = a
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
which is constant.
{{qed}}
Theorem: Pendulum Contained by Cycloid moves along Cycloidal Path

Let a pendulum with a flexible rod be suspended from a point $P$.
Let the rod be contained by a pair of bodies shaped as the arcs of a cycloid such that $P$ is the cusp between those two arcs.
:400px
Then the bob is constrained to move such that its path traces the arc of a cycloid.

Proof:
From Evolute of Cycloid is Cycloid, the evolute of a cycloid is another cycloid.
From Curve is Involute of Evolute, the involute of a cycloid is another cycloid as well.
But by the definition of involute, the path defined by the pendulum as described is the involute of the cycloid.
Hence the result.
{{qed}}