avewright/proofwiki-math huggingface dataset:
Theorem: Acceleration Vector in Polar Coordinates

Consider a particle $p$ moving in the plane.
Let the position of $p$ at time $t$ be given in polar coordinates as $\polar {r, \theta}$.
Then the acceleration $\mathbf a$ of $p$ can be expressed as:
:$\mathbf a = \paren {r \dfrac {\d^2 \theta} {\d t^2} + 2 \dfrac {\d r} {\d t} \dfrac {\d \theta} {\d t} } \mathbf u_\theta + \paren {\dfrac {\d^2 r} {\d t^2} - r \paren {\dfrac {\d \theta} {\d t} }^2} \mathbf u_r$
where:
:$\mathbf u_r$ is the unit vector in the direction of the radial coordinate of $p$
:$\mathbf u_\theta$ is the unit vector in the direction of the angular coordinate of $p$

Proof:
Let the radius vector $\mathbf r$ from the origin to $p$ be expressed as:
:$(1): \quad \mathbf r = r \mathbf u_r$
:600px
From Derivatives of Unit Vectors in Polar Coordinates:
{{begin-eqn}}
{{eqn | n = 2
      | l = \dfrac {\d \mathbf u_r} {\d \theta}
      | r = \mathbf u_\theta
      | c = 
}}
{{eqn | n = 3
      | l = \dfrac {\d \mathbf u_\theta} {\d \theta}
      | r = -\mathbf u_r
      | c = 
}}
{{end-eqn}}
From Velocity Vector in Polar Coordinates:
:$\mathbf v = r \dfrac {\d \theta} {\d t} \mathbf u_\theta + \dfrac {\d r} {\d t} \mathbf u_r$
where $\mathbf v$ is the velocity of $p$.
The acceleration of $p$ is by definition the rate of change in its velocity:
{{begin-eqn}}
{{eqn | l = \mathbf a
      | r = \dfrac {\d \mathbf v} {\d t}
      | c = 
}}
{{eqn | r = r \dfrac {\d^2 \theta} {\d t^2} \mathbf u_\theta + \dfrac {\d r} {\d t} \dfrac {\d \theta} {\d t} \mathbf u_\theta + r \dfrac {\d \theta} {\d t} \dfrac {\d \mathbf u_\theta} {\d t} + \dfrac {\d^2 r} {\d t^2} \mathbf u_r + \dfrac {\d r} {\d t} \dfrac {\d \mathbf u_r} {\d t}
      | c = Product Rule for Derivatives
}}
{{eqn | r = r \dfrac {\d^2 \theta} {\d t^2} \mathbf u_\theta + \dfrac {\d r} {\d t} \dfrac {\d \theta} {\d t} \mathbf u_\theta + r \dfrac {\d \theta} {\d t} \dfrac {\d \mathbf u_\theta} {\d \theta} \dfrac {\d \theta} {\d t} + \dfrac {\d^2 r} {\d t^2} \mathbf u_r + \dfrac {\d r} {\d t} \dfrac {\d \mathbf u_r} {\d \theta} \dfrac {\d \theta} {\d t}
      | c = Chain Rule for Derivatives
}}
{{eqn | r = r \dfrac {\d^2 \theta} {\d t^2} \mathbf u_\theta + \dfrac {\d r} {\d t} \dfrac {\d \theta} {\d t} \mathbf u_\theta - r \dfrac {\d \theta} {\d t} \mathbf u_r \dfrac {\d \theta} {\d t} + \dfrac {\d^2 r} {\d t^2} \mathbf u_r + \dfrac {\d r} {\d t} \mathbf u_\theta \dfrac {\d \theta} {\d t}
      | c = substituting from $(2)$ and $(3)$
}}
{{eqn | r = \paren {r \dfrac {\d^2 \theta} {\d t^2} + 2 \dfrac {\d r} {\d t} \dfrac {\d \theta} {\d t} } \mathbf u_\theta + \paren {\dfrac {\d^2 r} {\d t^2} - r \paren {\dfrac {\d \theta} {\d t} }^2} \mathbf u_r
      | c = gathering terms
}}
{{end-eqn}}
{{qed}}
Theorem: Eccentricity of Orbit indicates its Total Energy

Consider a planet $p$ of mass $m$ orbiting a star $S$ of mass $M$ under the influence of the gravitational field which the two bodies give rise to.
Then the total energy of the system determines the eccentricity of the orbit of $p$ around $S$.

Proof:
Let:
:$\mathbf u_r$ be the unit vector in the direction of the radial coordinate of $p$
:$\mathbf u_\theta$ be the unit vector in the direction of the angular coordinate of $p$.
By Kinetic Energy of Motion, the kinetic energy of $p$ is:
:$K = \dfrac {m v^2} 2$
where $v$ is the magnitude of the velocity of $p$.
Thus:
{{begin-eqn}}
{{eqn | l = K
      | r = \dfrac {m \mathbf v \cdot \mathbf v} 2
      | c = Dot Product of Vector with Itself
}}
{{eqn | r = \dfrac 1 2 m \paren {r \dfrac {\d \theta} {\d t} \mathbf u_\theta + \dfrac {\d r} {\d t} \mathbf u_r} \cdot \paren {r \dfrac {\d \theta} {\d t} \mathbf u_\theta + \dfrac {\d r} {\d t} \mathbf u_r}
      | c = Velocity Vector in Polar Coordinates
}}
{{eqn | n = 1
      | r = \dfrac 1 2 m \paren {r^2 \paren {\dfrac {\d \theta} {\d t} }^2 + \paren {\dfrac {\d r} {\d t} }^2}
      | c = {{Defof|Dot Product}}
}}
{{end-eqn}}
The potential energy $P$ of the system is the negative of the work required to move $p$ to infinity:
{{MissingLinks|Definition of Work, the above definition of P.E.}}
{{begin-eqn}}
{{eqn | l = P
      | r = -\int_r^\infty \dfrac {G M m} {r^2} \rd r
      | c = Newton's Law of Universal Gravitation
}}
{{eqn | r = \intlimits {\dfrac {G M m} r} r \infty
      | c = Primitive of Power
}}
{{eqn | r = -\dfrac {G M m} r
      | c = 
}}
{{eqn | n = 2
      | r = -\dfrac {k m} r
      | c = defining $k = G M$: constant for this system
}}
{{end-eqn}}
By the Principle of Conservation of Energy, the total energy in the system remains constant: $E$, say.
So:
:$E = \dfrac 1 2 m \paren {r^2 \paren {\dfrac {\d \theta} {\d t} }^2 + \paren {\dfrac {\d r} {\d t} }^2} - \dfrac {k m} r$
{{WLOG}}, let us arrange the polar axis so as to make $r$ a minimum when $\theta = 0$.
By Kepler's First Law of Planetary Motion, the position of $p$ in polar coordinates is:
:$(3): \quad r = \dfrac {h^2 / k} {1 + e \cos \theta}$
At the instant when $\theta = 0$, we therefore have:
:$r = \dfrac {h^2 / k} {1 + e}$
At this point, $r$ is at a local minimum.
Hence:
:$\dfrac {m r^2} 2 \dfrac {h^2} {r^4} - \dfrac {k m} r = E$
Eliminating $r$ from these gives:
:$e = \sqrt {1 + E \paren {\dfrac {2 h^2} {m k^2} } }$
Thus equation $(3)$ for the orbit of $p$ can be written as:
:$r = \dfrac {h^2 / k} {1 + \sqrt {1 + E \paren {2 h^2 / m k^2}} \cos \theta }$
Thus from Equation of Conic Section in Polar Form, it can be seen that the orbit is:
:an ellipse when $E < 0$
:a parabola when $E = 0$
:a hyperbola when $E > 0$.
{{qed}}
Theorem: Existence of Non-Empty Finite Suprema in Join Semilattice

Let $\struct {S, \preceq}$ be a join semilattice.
Let $A$ be a non-empty finite subset of $S$.
Then $A$ admits a supremum in $\struct {S, \preceq}$.

Proof:
We will prove by induction of the cardinality of finite subset of $H$.
Theorem: Variance of Exponential Distribution

Let $X$ be a continuous random variable with the exponential distribution with parameter $\beta$.
Then the variance of $X$ is:
:$\var X = \beta^2$

Proof:
From Variance as Expectation of Square minus Square of Expectation:
:$\var X = \expect {X^2} - \paren {\expect X}^2$
From Expectation of Exponential Distribution:
:$\expect X = \beta$
The expectation of $X^2$ is:
{{begin-eqn}}
{{eqn | l = \expect {X^2}
      | r = \int_{x \mathop \in \Omega_X} x^2 \, \map {f_X} x \rd x
      | c = {{Defof|Expectation of Continuous Random Variable}}
}}
{{eqn | r = \int_0^\infty x^2 \frac 1 \beta \map \exp {-\frac x \beta} \rd x
      | c = Probability Density Function of Exponential Distribution
}}
{{eqn | r = \intlimits {-x^2 \map \exp {-\frac x \beta} } 0 \infty + \int_0^\infty 2 x \map \exp {-\frac x \beta} \rd x
      | c = Integration by Parts
}}
{{eqn | r = 0 + 2 \beta \int_0^\infty x \frac 1 \beta \, \map \exp {-\frac x \beta} \rd x 
      | c = algebraic manipulation
}}
{{eqn | r = 2 \beta \, \expect X
      | c = Expectation of Exponential Distribution
}}
{{eqn | r = 2 \beta^2
}}
{{end-eqn}}
Thus the variance of $X$ is:
{{begin-eqn}}
{{eqn | l = \var X
      | r = \expect {X^2} - \paren {\expect X}^2
}}
{{eqn | r = 2 \beta^2 - \beta^2 
}}
{{eqn | r = \beta^2
}}
{{end-eqn}}
{{qed}}
Theorem: Variance of Exponential Distribution

Let $X$ be a continuous random variable with the exponential distribution with parameter $\beta$.
Then the variance of $X$ is:
:$\var X = \beta^2$

Proof:
By Moment Generating Function of Exponential Distribution, the moment generating function $M_X$ of $X$ is given by: 
:$\map {M_X} t = \dfrac 1 {1 - \beta t}$ 
From Variance as Expectation of Square minus Square of Expectation:
:$\var X = \expect {X^2} - \paren {\expect X}^2$ 
From Moment in terms of Moment Generating Function, we also have: 
:$\expect {X^2} = \map {M_X' '} 0$
In Expectation of Exponential Distribution: Proof 2, it is shown that: 
:$\map {M_X'} t = \dfrac \beta {\paren {1 - \beta t}^2}$ 
We have: 
{{begin-eqn}}
{{eqn | l = \map {M_X' '} t
      | r = \frac \d {\d t} \paren {\frac \beta {\paren {1 - \beta t}^2} }
}}
{{eqn | r = \frac {2 \beta^2} {\paren {1 - \beta t}^3}
      | c = Chain Rule for Derivatives, Derivative of Power 
}}
{{end-eqn}} 
Setting $t = 0$ gives: 
{{begin-eqn}}
{{eqn | l = \expect {X^2}
      | r = \frac {2 \beta^2} {\paren {1 - 0 \beta}^3}
}}
{{eqn | r = 2 \beta^2
}}
{{end-eqn}}
By Expectation of Exponential Distribution, we have: 
:$\expect X = \beta$
So: 
{{begin-eqn}}
{{eqn | l = \var X
      | r = 2 \beta^2 - \beta^2
}}
{{eqn | r = \beta^2
}}
{{end-eqn}}
{{qed}}
Theorem: Cardinality of Singleton

Let $A$ be a set.
Then $\card A = 1$ {{iff}} $\exists a: A = \set a$
where $\card A$ denotes the cardinality of $A$.

Proof:
=== Sufficient Condition ===
Assume that
:$\card A = 1$
By definition of cardinality of finite set:
:$A \sim \N_{< 1} = \set 0$
where $\sim$ denotes set equivalence.
By Set Equivalence behaves like Equivalence Relation:
:$\set 0 \sim A$
By definition of set equivalence there exists a bijection:
:$f: \set 0 \to A$
By definition of bijection:
:$f$ is s surjection.
Thus
{{begin-eqn}}
{{eqn | l = A
      | r = \map {f^\to} {\set 0}
      | c = {{Defof|Surjection}}
}}
{{eqn | r = \set {\map f 0}
      | c = Image of Singleton under Mapping
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Existence of Non-Empty Finite Infima in Meet Semilattice

Let $\struct {S, \preceq}$ be a meet semilattice.
Let $A$ be a non-empty finite subset of $S$.
Then $A$ admits a infimum in $\struct {S, \preceq}$.

Proof:
This follows by {{mutatis}} of the proof of Existence of Non-Empty Finite Suprema in Join Semilattice.
{{qed}}
Theorem: Circle is Bisected by Diameter

A circle is bisected by a diameter.

Proof:
Let $AB$ be a diameter of a circle $ADBE$ whose center is at $C$.
By definition of diameter, $AB$ passes through $C$.
{{AimForCont}} that $AB$ does not bisect $ADBE$, but that $ADBC$ is larger than $AEBC$.
:400px
Thus it will be possible to find a diameter $DE$ passing through $C$ such that $DC \ne CE$.
Both $DC$ and $CE$ are radii of $ADBE$.
By Euclid's definition of the circle:
:''{{:Definition:Euclid's Definitions - Book I/15 - Circle}}''
:''{{:Definition:Euclid's Definitions - Book I/16 - Center of Circle}}''
That is, all radii of $ADBE$ are equal.
But $DC \ne CE$.
From this contradiction it follows that $AB$ bisects the circle.
{{qed}}
Theorem: Circle is Bisected by Diameter

A circle is bisected by a diameter.

Proof:
:400px
Let $AB$ be a diameter of a circle whose center is at $O$.
By definition of diameter, $AB$ passes through $O$.
$\angle AOB\cong\angle BOA$ because they are both straight angles.
Thus, the arcs are congruent by Equal Angles in Equal Circles:
:$\stackrel{\frown}{AB}\cong\stackrel{\frown}{BA}$
Hence, a circle is split into two equal arcs by a diameter.
{{qed}}
Theorem: External Angle of Triangle equals Sum of other Internal Angles

The external angle of a triangle equals the sum of the other two internal angles.
{{:Euclid:Proposition/I/32}}

Proof:
:300px
Let $\triangle ABC$ be a triangle.
Let $BC$ be extended to a point $D$.
Construct $CE$ through the point $C$ parallel to the straight line $AB$.
We have that $AB \parallel CE$ and $AC$ is a transversal that cuts them.
From Parallelism implies Equal Alternate Angles:
:$\angle BAC = \angle ACE$
Similarly, we have that $AB \parallel CE$ and $BD$ is a transversal that cuts them.
From Parallelism implies Equal Corresponding Angles:
:$\angle ECD = \angle ABC$
Thus by Euclid's Second Common Notion:
: $\angle ACD = \angle ABC + \angle BAC$
{{qed}}
Theorem: External Angle of Triangle equals Sum of other Internal Angles

The external angle of a triangle equals the sum of the other two internal angles.
{{:Euclid:Proposition/I/32}}

Proof:
Let $\triangle ABC$ be a triangle.
From Sum of Angles of Triangle equals Two Right Angles: Proof 2:
:$\paren 1: \angle ABC + \angle BCA + \angle CAB = 180^\circ$
Extend $AB$ to $D$.
By Two Angles on Straight Line make Two Right Angles:
:$\paren 1: \angle ABC + \angle CBD = 180^\circ$
Combining $\paren 1$ and $\paren 2$ and using Equality is Transitive:
:$\angle ABC + \angle BCA + \angle CAB = \angle ABC + \angle CBD$
By using commom notion 3:
:$\angle BCA + \angle CAB = \angle CBD$
By using Equality is Symmetric:
:$\angle CBD = \angle BCA + \angle CAB$
{{qed}}
Theorem: First Pappus-Guldinus Theorem

Let $C$ be a plane figure that lies entirely on one side of a straight line $\LL$.
Let $S$ be the solid of revolution generated by $C$ around $\LL$.
Then the volume of $S$ is equal to the area of $C$ multiplied by the distance travelled by the centroid of $C$ around $\LL$ when generating $S$.

Proof:
Let $V$ denote the volume of $S$
Let $\AA$ denote the area of $C$.
Let $C$ be embedded in a Cartesian plane such that $\LL$ coincides with the $x$-axis.
Let $\tuple {\overline x, \overline y}$ be the coordinates of the centroid of $C$.
Consider a rectangle $R$ bounded by the lines:
:$y = 0$
:$x = \xi$
:$x = \xi + \delta x$
:$y = \map f x$
The moment $M_y$ of $R$ about the $y$-axis is given by:
:$M_y = \map f x \xi \rdelta \xi$
Hence from Area under Curve:
:$\AA \overline x = \ds \int_a^b x \map f x \rd x$
The moment $M_x$ of $R$ about the $x$-axis is given by:
:$M_x = y \rdelta x \dfrac y 2$
that is, half way up.
Hence:
:$\AA \overline y = \dfrac 1 2 \ds \int_a^b y^2 \rd x$
It follows immediately that:
:$\dfrac V \AA \overline y = 2 \pi$
That is:
:$V = 2 \pi \AA \overline y$
{{questionable|The above is the exposition given in {{BookReference|A Note Book in Pure Mathematics||L. Harwood Clarke}}. It is based on an unstated assumption that $C$ is bounded on one side by the $x$ axis, which is not necessarily the case. I will get round to hunting down a rigorous exposition of this. I must have it on my bookshelf somewhere in one of my mechanics texts. If anyone wants to take this on and make it rigorous, feel free to do so.}}
Theorem: Pythagoras's Theorem for Parallelograms

Let $\triangle ABC$ be a triangle.
Let $ACDE$ and $BCFG$ be parallelograms constructed on the sides $AC$ and $BC$ of $\triangle ABC$.
Let $DE$ and $FG$ be produced to intersect at $H$.
Let $AJ$ and $BI$ be constructed on $A$ and $B$ parallel to and equal to $HC$.
Then the area of the parallelogram $ABIJ$ equals the sum of the areas of the parallelograms $ACDE$ and $BCFG$.

Proof:
:400px
From Parallelograms with Same Base and Same Height have Equal Area:
:$ACDE = ACHR = ATUJ$
and:
:$BCFG = BCHS = BIUT$
Hence the result.
{{qed}}
Theorem: Volume of Sphere from Surface Area

The volume $V$ of a sphere of radius $r$ is given by:
:$V = \dfrac {r A} 3$
where $A$ is the surface area of the sphere.

Proof:
Let the surface of the sphere of radius $r$ be divided into many small areas.
If they are made small enough, they can be approximated to plane figures.
Let the areas of these plane figures be denoted:
:$a_1, a_2, a_3, \ldots$
Let the sphere of radius $r$ be divided into as many pyramids whose apices are at the center and whose bases are these areas.
From Volume of Pyramid, their volumes are:
:$\dfrac {r a_1} 3, \dfrac {r a_2} 3, \dfrac {r a_3} 3, \ldots$
The volume $\VV$ of the sphere is given by the sum of the volumes of each of these pyramids:
{{begin-eqn}}
{{eqn | l = \VV
      | r = \dfrac {r a_1} 3 + \dfrac {r a_2} 3 + \dfrac {r a_3} 3 + \cdots
      | c = 
}}
{{eqn | r = \dfrac r 3 \paren {a_1 + a_2 + a_3 + \cdots}
      | c = 
}}
{{end-eqn}}
But $a_1 + a_2 + a_3 + \cdots$ is the surface area of the sphere.
Hence:
{{begin-eqn}}
{{eqn | l = \VV
      | r = \dfrac r 3 \paren {a_1 + a_2 + a_3 + \cdots}
      | c = 
}}
{{eqn | r = \dfrac r 3 A
      | c = 
}}
{{end-eqn}}
It needs to be noted that this proof is intuitive and non-rigorous.
{{qed}}
Theorem: Lower Bound is Lower Bound for Subset

Let $\struct {S, \preceq}$ be a preordered set.
Let $A, B$ be subsets of $S$ such that
:$B \subseteq A$
Let $L$ be an element of $S$.
Let $L$ be a lower bound for $A$.
Then $L$ is a lower bound for $B$.

Proof:
Let $L$ be a lower bound for $A$.
By definition of lower bound:
:$\forall x \in A: L \preceq x$
By definition of subset:
:$\forall x \in B: x \in A$
Hence:
:$\forall x \in B: L \preceq x$
Thus by definition:
:$L$ is a lower bound for $B$.
{{qed}}
Theorem: Upper Bound is Upper Bound for Subset

Let $\left({S, \preceq}\right)$ be a preordered set.
Let $A, B$ be subsets of $S$ such that
:$B \subseteq A$
Let $U$ be an upper bound for $A$.
Then $U$ is an upper bound for $B$.

Proof:
Assume that:
: $U$ is upper bound for $A$.
By definition of upper bound:
:$\forall x \in A: x \preceq U$
By definition of subset:
:$\forall x \in B: x \in A$
Hence:
:$\forall x \in B: x \preceq U$
Thus by definition
: $U$ is sn upper bound for $B$.
{{qed}}
Theorem: Largest Rectangle with Given Perimeter is Square

Let $\SS$ be the set of all rectangles with a given perimeter $L$.
The element of $\SS$ with the largest area is the square with length of side $\dfrac L 4$.

Proof:
Consider an arbitrary element $R$ of $\SS$.
Let $B$ be half the perimeter of $R$.
Let $x$ be the length of one side of $R$.
Then the length of an adjacent side is $B - x$.
The area $\AA$ of $R$ is then given by:
:$\AA = x \paren {B - x}$
Let $\AA$ be expressed in functional notation as:
:$\map f x = x \paren {B - x}$
We have:
{{begin-eqn}}
{{eqn | l = \map f {x + E} - \map f x
      | r = \paren {x + E} \paren {B - \paren {x + E} } - x \paren {B - x}
      | c = 
}}
{{eqn | r = E B - 2 E x - E^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\map f {x + E} - \map f x} E
      | r = B - 2 x - E
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \intlimits {\frac {\map f {x + E} - \map f x} E} {E \mathop = 0} {}
      | r = B - 2 x
      | c = 
}}
{{end-eqn}}
Thus from the Interior Extremum Theorem, when $B - 2 x = 0$, the area of $R$ is at a maximum or a minimum.
That is:
:$x = \dfrac B 2 = \dfrac L 4$
Geometrical analysis shows that for this length of side the area is not a minimum because that happens when $x = 0$ or $x = B$.
Hence the result.
{{qed}}
Theorem: Mapping Preserves Finite and Directed Suprema

Let $\struct {S_1, \preceq_1}$ and $\struct {S_2, \preceq_2}$ be join semilattices.
Let $f: S_1 \to S_2$ be a mapping.
Let $f$ preserve finite suprema and preserve directed suprema.
Then $f$ also preserves all suprema

Proof:
This follows by {{mutatis}} of the proof of Mapping Preserves Finite and Filtered Infima.
{{qed}}
Theorem: Integer as Sum of Polygonal Numbers

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then $n$ is:
:$(1): \quad$ Either triangular or the sum of $2$ or $3$ triangular numbers
:$(2): \quad$ Either square or the sum of $2$, $3$ or $4$ square numbers
:$(3): \quad$ Either pentagonal or the sum of $2$, $3$, $4$ or $5$ pentagonal numbers
:and so on.
That is:
:for all $k \ge 3$, $n$ is the sum of no more than $k$ polygonal numbers of order $k$.

Proof:
First some lemmata:
Theorem: Infima Preserving Mapping on Filters is Increasing

Let $\struct {S, \preceq}$, $\struct {T, \precsim}$ be ordered sets.
Let $f: S \to T$ be a mapping.
For every filter $F$ in $\struct {S, \preceq}$, let $f$ preserve the infimum on $F$.
Then $f$ is increasing.

Proof:
Let $x, y \in S$ such that:
:$x \preceq y$
By Infimum of Singleton:
:$\set x$ and $\set y$ admit infima in $\struct {S, \preceq}$
By Infimum of Upper Closure of Set:
:$\set x^\succeq$ and $\set y^\succeq$ admit infima in $\struct {S, \preceq}$
where $\set x^\succeq$ denotes the upper closure of $\set x$.
By Upper Closure of Singleton
:$x^\succeq$ and $y^\succeq$ admit infima in $\struct {S, \preceq}$
By Upper Closure of Element is Filter:
:$x^\succeq$ and $y^\succeq$ are filter in $\struct {S, \preceq}$
By assumption and definition of mapping preserves the infimum on subset:
:$\map {f^\to} {x^\succeq}$ and $\map {f^\to} {y^\succeq}$ admit infima in $\struct {T, \precsim}$
and
:$\inf \set {\map {f^\to} {x^\succeq} } = \map f {\inf \set {x^\succeq} }$ and $\inf \set {\map {f^\to} {y^\succeq} } = \map f {\inf \set {y^\succeq} }$
By Infimum of Upper Closure of Element:
:$\inf \set {x^\succeq} = x$ and $\inf \set {y^\succeq} = y$
By Upper Closure is Decreasing:
:$y^\succeq \subseteq x^\succeq$
By Image of Subset under Mapping is Subset of Image:
:$\map {f^\to} {y^\succeq} \subseteq \map {f^\to} {x^\succeq}$
Thus by Infimum of Subset:
:$\map f x \precsim \map f y$
Thus by definition:
:$f$ is increasing.
{{qed}}
Theorem: Infimum of Upper Closure of Set

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$.
Let $U = T^\succeq$ be the upper closure of $T$ in $S$.
Let $s \in S$.
Then $s$ is the infimum of $T$ {{iff}} it is the infimum of $U$.

Proof:
This follows by {{mutatis}} of the proof of Supremum of Lower Closure of Set.
{{qed}}
Theorem: Cavalieri's Principle/Extension

Let two solid figures $S_1$ and $S_2$ have equal height.
Let the areas of the sections made by planes parallel to their bases and at equal distances from the bases always have the same ratio.
Then the volumes of $S_1$ and $S_2$ are in that same ratio.

Proof:
{{ProofWanted}}
{{Namedfor|Bonaventura Francesco Cavalieri|cat = Cavalieri}}
Theorem: Cavalieri's Principle

Let two solid figures $S_1$ and $S_2$ have equal height.
Let sections made by planes parallel to their bases and at equal distances from the bases always have equal area.
Then the volumes of $S_1$ and $S_2$ are equal.

Proof:
Let $H$ be the common height of the two figures.
The volume of a solid figure is its Lebesgue Measure in $\R^3$.
{{TheoremWanted|The above needs to be demonstrated as it is in fact is the core of the principle}}
Therefore:
{{begin-eqn}}
{{eqn | l = \map V {S_1}
      | r = \map {\lambda^3} {S_1}
}}
{{eqn | r = \int_{\R^3} \chi_{S_1} \rd \lambda^3
      | c = {{Defof|Integral of Positive Simple Function}}
}}
{{eqn | r = \int_{\R \times \R^2} \chi_{S_1} \rd \paren {\lambda \times \lambda^2}
}}
{{eqn | r = \int_\R \int_{\R^2} \paren {\chi_{S_1} }_x \rd \lambda^2 \rd \lambda
      | c = Fubini's Theorem
}}
{{eqn | r = \int_{\closedint 0 H} \int_{\R^2} \paren {\chi_{S_1} }_x \rd \lambda^2 \rd \lambda
      | c = Figure is bounded between planes $x = 0$ and $x = H$
}}
{{end-eqn}}
{{Explain|Lebesgue measure isn't a product measure. We need a variant of Fubini that works on completions of measure spaces.}}
In the same manner:
:$\ds \map V {S_2} = \int_{\closedint 0 H} \int_{\R^2} \paren {\chi_{S_2} }_x \rd \lambda^2 \rd \lambda$
The area of a plane figure is its Lebesgue Measure in $\R^2$.
The area of a section made in $S_1$ by the plane $x = x_0$ is:
{{begin-eqn}}
{{eqn | l = \map A {S_1 \cap P_{x \mathop = x_0} }
      | r = \map {\lambda^2} {S_1 \cap P {x = x_0} }
}}
{{eqn | r = \int_{\R^2} \paren {\chi_{S_1} }_{x \mathop = x_0} \rd \lambda^2
      | c = {{Defof|Integral of Positive Simple Function}}
}}
{{end-eqn}}
Likewise:
:$\ds \map A {S_2 \cap P_{x \mathop = x_0} } = \int_{\R^2} \paren {\chi_{S_2} }_{x \mathop = x_0} \rd \lambda^2$
But by assumption:
:$\map A {S_1 \cap P_{x \mathop = x_0} } = \map A {S_2 \cap P_{x \mathop = x_0} }$
for every $x_0 \in \closedint 0 H$.
Therefore:
{{begin-eqn}}
{{eqn | ll= \leadsto
      | l = \int_{\R^2} \paren {\chi_{S_1} }_x \rd \lambda^2
      | r = \int_{\R^2} \paren {\chi_{S_2} }_x \rd \lambda^2
}}
{{eqn | l = \int_{\closedint 0 H} \int_{\R^2} \paren {\chi_{S_1} }_x \rd \lambda^2 \rd \lambda
      | r = \int_{\closedint 0 H} \int_{\R^2} \paren {\chi_{S_2} }_x \rd \lambda^2 \rd \lambda
}}
{{end-eqn}}
Thus we conclude that $\map V {S_1} = \map V {S_2}$
{{qed}}
{{Namedfor|Bonaventura Francesco Cavalieri|cat = Cavalieri}}
Theorem: Volume of Cone

Let $K$ be a cone whose base is of area $A$ and whose height is $h$.
Then the volume of $K$ is given by:
:$V_K = \dfrac {A h} 3$

Proof:
Let $V_K$ be the volume of $K$.
Let $V_C$ be the volume of a cylinder of base $A$ and of height $h$.
From Volume of Cylinder in terms of Height and Base Area:
:$V_C = A h$
From Volume of Cone is Third of Cylinder on Same Base and of Same Height:
{{begin-eqn}}
{{eqn | l = V_K
      | r = \dfrac {V_C} 3
      | c = 
}}
{{eqn | r = \dfrac {A h} 3
      | c = 
}}
{{end-eqn}}
{{qed}}