avewright/proofwiki-math huggingface dataset:
Theorem: Empty Set as Subset

Let $S$ be a set.
Let $A$ be a subset of $S$.
Then:
:$A = \O \iff \forall x \in S: x \notin A$

Proof:
Sufficient condition follows by definition of empty set.
For necessary condition assume that:
:$\forall x \in S: x \notin A$
Let $x$ be arbitrary.
{{AimForCont}} that:
:$x \in A$
By definition of subset:
:$x \in S$
By assumption:
:$x \notin A$
Thus this contradicts:
:$x \in A$
{{qed}}
Category:Empty Set
Category:Subsets
g8jdogbcwe1pt3da9kpvz5dgt1njjio
Theorem: Pythagorean Triangles whose Areas are Repdigit Numbers

The following Pythagorean triangles have areas consisting of repdigit numbers:

Proof:
From Pythagorean Triangle whose Area is Half Perimeter, the area of the $3-4-5$ triangle is $6$, which is trivially repdigit.
The next Pythagorean triangles in area are:
:the $6-8-10$ triangle, which has area $\dfrac {6 \times 8} 2 = 24$
:the $5-2-13$ triangle, which has area $\dfrac {5 \times 12} 2 = 30$
So there are no more Pythagorean triangles whose areas consist of a single digit.
We have that the $693-1924-2045$ triangle is Pythagorean.
Then its area $A$ is given by:
{{begin-eqn}}
{{eqn | l = A
      | r = \dfrac {693 \times 1924} 2
      | c = 
}}
{{eqn | r = \dfrac {\paren {3^2 \times 7 \times 11} \times \paren {2^2 \times 13 \times 37} } 2
      | c = 693 and 1924
}}
{{eqn | r = \paren {2 \times 3} \times \paren {3 \times 37} \times \paren {7 \times 11 \times 13}
      | c = 
}}
{{eqn | r = 6 \times 111 \times 1001
      | c = 6, 111 and 1001
}}
{{eqn | r = 666 \, 666
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of Series Equals Infinite Product

Let $\sequence {z_n}$ be a sequence of complex numbers.
Suppose $\ds \sum_{n \mathop = 1}^\infty z_n$ converges to $z \in \C$.
Then $\ds \prod_{n \mathop = 1}^\infty \map \exp {z_n}$ converges to $\exp z$.

Proof:
Let $S_n$ be the $n$th partial sum of $\ds \sum_{n \mathop = 1}^\infty z_n$.
Let $P_n$ be the $n$th partial product of $\ds \prod_{n \mathop = 1}^\infty \map \exp {z_n}$.
By Exponential of Sum, $\map \exp {S_n} = P_n$ for all $n \in \N$.
By Exponential Function is Continuous, $\ds \lim_{n \mathop \to \infty} \map \exp {S_n} = \exp z$.
By Exponential of Complex Number is Nonzero, $\exp z \ne 0$.
Thus $\ds \lim_{n \mathop \to \infty} P_n = \exp z \ne 0$.
{{qed}}
Theorem: Convergence of Series of Complex Numbers by Real and Imaginary Part

Let $\sequence {z_n}$ be a sequence of complex numbers.
Then:
:the series $\ds \sum_{n \mathop = 1}^\infty z_n$ converges to $Z \in \C$
{{iff}}:
:the series:
::$\ds \sum_{n \mathop = 1}^\infty \map \Re {z_n}$
:and:
::$\ds \sum_{n \mathop = 1}^\infty \map \Im {z_n}$
:converge to $\map \Re Z$ and $\map \Im Z$ respectively.

Proof:
Let:
:the $n$th partial sum of $\sequence {z_n}$ be denoted $Z_n$
:the $n$th partial sum of $\sequence {\map \Re {z_n} }$ be denoted $U_n$
:the $n$th partial sum of $\sequence {\map \Im {z_n} }$ be denoted $V_n$
Then:
:$Z_n = U_n + i V_n$
Let:
:$\ds \lim_{n \mathop \to \infty} U_n = U$
:$\ds \lim_{n \mathop \to \infty} V_n = V$
By definition of convergent complex sequence:
:$\ds \lim_{n \mathop \to \infty} Z_n = \lim_{n \mathop \to \infty} U_n + i \lim_{n \mathop \to \infty} V_n$
and so:
:$\ds \lim_{n \mathop \to \infty} Z_n = U + i V$
and the result follows.
{{Qed}}
Theorem: Lower Closure of Element is Closed under Directed Suprema

Let $L = \struct {S, \preceq}$ be an up-complete ordered set.
Let $x \in S$.
Then $x^\preceq$ is closed under directed suprema,
where $x^\preceq$ denotes the lower closure of $x$.

Proof:
Let $D$ be a directed subset of $S$ such that
:$D \subseteq x^\preceq$
By Lower Closure of Element is Ideal:
:$x^\preceq$ is directed.
By definition of up-complete:
:$D$ and $x^\preceq$ admit suprema.
By Supremum of Subset:
:$\sup D \preceq \map \sup {x^\preceq}$
By Supremum of Lower Closure of Element:
:$\sup D \preceq x$
Thus by definition of lower closure of element:
:$\sup D \in x^\preceq$
{{qed}}
Theorem: Pythagorean Triangle whose Hypotenuse and Leg differ by 1

Let $P$ be a Pythagorean triangle whose sides correspond to the Pythagorean triple $T$.
Then:
: the hypotenuse of $P$ is $1$ greater than one of its legs
{{iff}}:
: the generator for $T$ is of the form $G = \tuple {n, n + 1}$ where $n \in \Z_{> 0}$ is a (strictly) positive integer.

Proof:
We have from Solutions of Pythagorean Equation that the set of all primitive Pythagorean triples is generated by:
:$\tuple {2 m n, m^2 - n^2, m^2 + n^2}$
where $m, n \in \Z$ such that:
:$m, n \in \Z_{>0}$ are (strictly) positive integers
:$m \perp n$, that is, $m$ and $n$ are coprime
:$m$ and $n$ are of opposite parity
:$m > n$.
Theorem: Generator for Almost Isosceles Pythagorean Triangle

Let $P$ be a Pythagorean triangle whose sides correspond to the Pythagorean triple $T = \tuple {a, b, c}$.
Let the generator for $T$ be $\tuple {m, n}$.
Then:
:$P$ is almost isosceles
{{iff}}
:$\tuple {2 m + n, m}$ is the generator for the Pythagorean triple $T'$ of another almost isosceles Pythagorean triangle $P'$.

Proof:
By definition of almost isosceles:
:$\size {a - b} = 1$
First note that, from Consecutive Integers are Coprime, an almost isosceles Pythagorean triangle is a primitive Pythagorean triangle.
Hence $T$ and $T'$ are primitive Pythagorean triples.
Thus it is established that by Solutions of Pythagorean Equation, both $P$ and $P'$ are of the form:
:$\tuple {2 m n, m^2 + n^2, m^2 - n^2}$
for some $m, n \in \Z_{>0}$ where:
:$m > n$
:$m \perp n$
:$m$ and $n$ are of opposite parity.
Theorem: Kusmin-Landau Inequality

Let $I$ be the half-open interval $\hointl a b$.
Let $f: I \to R$ be continuously differentiable.
Let $f'$ be monotonic.
Let $\norm {f'} \ge \lambda$ on $I$ for some $\lambda \in \R_{>0}$, where $\norm {\, \cdot \,}$ denotes the distance to nearest integer.
Then:
:$\ds \sum_{n \mathop \in I} e^{2 \pi i \map f n} = \map \OO {\frac 1 \lambda}$
where the big-$\OO$ estimate does not depend on $f$.
{{explain|What does the sum over an interval $I$ mean?}}

Proof:
{{ProofWanted}}
{{Namedfor|Rodion Osievich Kuzmin|name2 = Edmund Georg Hermann Landau|cat = Kuzmin|cat2 = Landau}}
Theorem: Closure of Singleton is Lower Closure of Element in Scott Topological Lattice

Let $T = \struct {S, \preceq, \tau}$ be a up-complete topological lattice with the Scott topology.
Let $x \in S$.
Then:
:$\set x^- = x^\preceq$
where
:$\set x^-$ denotes the topological closure of $\set x$
:$x^\preceq$ denotes the lower closure of $x$.

Proof:
By Lower Closure of Element is Closed under Directed Suprema:
:$x^\preceq$ is closed under directed suprema.
By Lower Closure of Singleton:
:$\set x^\preceq = x^\preceq$
By Lower Closure is Lower Section:
:$x^\preceq$ is a lower section.
By Closed Set iff Lower and Closed under Directed Suprema in Scott Topological Ordered Set:
:$x^\preceq$ is closed.
By definitions of lower closure of element and reflexivity:
:$x \in x^\preceq$
By Singleton of Element is Subset:
:$\set x \subseteq x^\preceq$
We will prove that:
:for every a closed subset $C$ of $S$: $\set x \subseteq C \implies x^\preceq \subseteq C$
Let $C$ be a closed subset of $S$ such that:
:$\set x \subseteq C$
By Closed Set iff Lower and Closed under Directed Suprema in Scott Topological Ordered Set:
:$C$ is a lower section.
Let $y \in x^\preceq$.
By definition of lower closure of element:
:$y \preceq x$
By definitions of subset and singleton:
:$x \in C$
Thus by definition of lower section:
:$y \in C$
{{qed|lemma}}
Thus by definition of topological closure:
:$\set x^- = x^\preceq$
{{qed}}
Theorem: Pythagorean Triangle cannot be Isosceles

Let $P$ be a Pythagorean triangle.
Then $P$ is not isosceles.

Proof:
Let $P$ be a Pythagorean triangle.
{{AimForCont}} $P$ is isosceles.
Let the legs of $P$ be of length $a$.
Let the hypotenuse of $P$ be of length $h$.
We have from Pythagoras's Theorem that:
:$2 a^2 = h^2$
and so:
:$\dfrac h a = \sqrt 2$
By definition, $h$ and $a$ are integers.
Hence, by definition, $\sqrt 2$ is a rational number.
But that contradicts the result Square Root of 2 is Irrational.
By Proof by Contradiction, it follows that $P$ cannot be isosceles.
{{qed}}
Theorem: Brahmagupta-Fibonacci Identity/Corollary

:$\paren {a^2 + b^2} \paren {c^2 + d^2} = \paren {a c - b d}^2 + \paren {a d + b c}^2$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {a^2 + b^2} \paren {c^2 + d^2}
      | r = \paren {a c + b d}^2 + \paren {a d - b c}^2
      | c = Brahmagupta-Fibonacci Identity
}}
{{eqn | ll= \leadsto
      | l = \paren {a^2 + \paren {-b}^2} \paren {c^2 + d^2}
      | r = \paren {a c + \paren {-b} d}^2 + \paren {a d - \paren {-b} c}^2
      | c = substituting $-b$ for $b$
}}
{{eqn | ll= \leadsto
      | l = \paren {a^2 + b^2} \paren {c^2 + d^2}
      | r = \paren {a c - b d}^2 + \paren {a d + b c}^2
      | c = 
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Brahmagupta|name2 = Leonardo Fibonacci}}
Theorem: Scott Topological Lattice is T0 Space

Let $T = \struct {S, \preceq, \tau}$ be a complete topological lattice with Scott topology.
Then $T$ is a $T_0$ space.

Proof:
Let $x, y \in S$ such that:
:$x \ne y$
By Closure of Singleton is Lower Closure of Element in Scott Topological Lattice:
:$\set x^- = x^\preceq$ and $\set y^- = y^\preceq$
Thus by Lower Closures are Equal implies Elements are Equal:
:$\set x^- \ne \set y^-$
Hence by Characterization of T0 Space by Distinct Closures of Singletons:
:$T$ is $T_0$ space.
{{qed}}
Theorem: Lower Closures are Equal implies Elements are Equal

Let $L = \struct {S, \preceq}$ be an ordered set.
Let $x, y \in S$ such that
:$x^\preceq = y^\preceq$
where $x^\preceq$ denotes the lower closure of $x$.
Then $x = y$

Proof:
By definitions of lower closure of element and reflexivity:
:$x \in x^\preceq$ and $y \in y^\preceq$
By definition of lower closure of element:
:$x \preceq y$ and $y \preceq x$
Thus by definition of antisymmetry:
:$x = y$
{{qed}}
Theorem: Square of Pythagorean Prime is Hypotenuse of Pythagorean Triangle

Let $p$ be a Pythagorean prime.
Then $p^2$ is the hypotenuse of a Pythagorean triangle.

Proof:
By Fermat's Two Squares Theorem, a Pythagorean prime, $p$ can be expressed in the form:
:$p = m^2 + n^2$
where $m$ and $n$ are (strictly) positive integers.
:$(1): \quad m \ne n$, otherwise $p$ would be of the form $2 m^2$ and so even and therefore not a prime.
:$(2): \quad m \perp n$, otherwise $\exists c \in \Z: p = c^2 \paren {p^2 + q^2}$ for some $p, q \in \Z$ and therefore not a prime.
:$(3): \quad m$ and $n$ are of opposite parity, otherwise $p = m^2 + n^2$ is  even and therefore not a prime.
{{WLOG}}, let $m > n$.
From Solutions of Pythagorean Equation, the triple $\tuple {2 m n, m^2 - n^2, m^2 + n^2}$ forms a primitive Pythagorean triple such that $m^2 + n^2$ forms the hypotenuse of a primitive Pythagorean triangle.
Thus we have that $p^2 = r^2 + s^2$ for some (strictly) positive integers $r$ and $s$.
Similarly, we have that $r \ne s$, otherwise $p^2$ would be of the form $2 r^2$ and so not a square number.
{{WLOG}}, let $r > s$.
From Solutions of Pythagorean Equation, the triple $\tuple {2 r s, r^2 - s^2, r^2 + s^2}$ forms a Pythagorean triple such that $p^2 = r^2 + s^2$ forms the hypotenuse of a Pythagorean triangle.
{{qed}}
Theorem: Pythagorean Triangle from Sum of Reciprocals of Consecutive Same Parity Integers

Let $a, b \in \Z_{>0}$ be (strictly) positive integers such that they are consecutively of the same parity.
Let $\dfrac p q = \dfrac 1 a + \dfrac 1 b$.
Then $p$ and $q$ are the legs of a Pythagorean triangle.

Proof:
Let $a$ and $b$ both be even.
Then:
{{begin-eqn}}
{{eqn | l = a
      | r = 2 n
      | c = 
}}
{{eqn | l = b
      | r = 2 \paren {n + 1}
      | c = for some $n \in \Z_{>0}$
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 a + \dfrac 1 b
      | r = \dfrac 1 {2 n} + \dfrac 1 {2 \paren {n + 1} }
      | c = 
}}
{{eqn | r = \dfrac {n + \paren {n + 1} } {2 n \paren {n + 1} }
      | c = 
}}
{{eqn | r = \dfrac {2 n + 1} {2 n \paren {n + 1} }
      | c = 
}}
{{eqn | r = \dfrac {n^2 + 2 n + 1 - n^2} {2 n \paren {n + 1} }
      | c = 
}}
{{eqn | r = \dfrac {\paren {n + 1}^2 - n^2} {2 n \paren {n + 1} }
      | c = 
}}
{{end-eqn}}
From Solutions of Pythagorean Equation, $\tuple {n, n + 1}$ form the generator for the primitive Pythagorean triple $\tuple {2 m n, m^2 - n^2, m^2 + n^2}$ where $m = n + 1$.
The legs of the resulting primitive Pythagorean triangle are $2 n \paren {n + 1}$ and $\paren {n + 1}^2 - n^2$.
Let $a$ and $b$ both be odd.
Then:
{{begin-eqn}}
{{eqn | l = a
      | r = 2 n + 1
      | c = 
}}
{{eqn | l = b
      | r = 2 \paren {n + 1} + 1
      | c = for some $n \in \Z_{>0}$
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 a + \dfrac 1 b
      | r = \dfrac 1 {2 n + 1} + \dfrac 1 {2 \paren {n + 1} + 1}
      | c = 
}}
{{eqn | r = \dfrac {4 n + 4} {4 n^2 + 8 n + 3}
      | c = 
}}
{{eqn | r = \dfrac {2 \paren {2 n + 2} \times 1} {\paren {2 n + 2}^2 - 1}
      | c = 
}}
{{end-eqn}}
From Solutions of Pythagorean Equation, $\tuple {2 n + 2, 1}$ form the generator for the primitive Pythagorean triple $\tuple {2 m n, m^2 - n^2, m^2 + n^2}$ where $m = 2 n + 2$ and $n = 1$.
The legs of the resulting primitive Pythagorean triangle are $2 \paren {2 n + 2}$ and $\paren {2 n + 2}^2 - 1$.
{{qed}}
Theorem: Legs of Pythagorean Triangle used as Generator for another Pythagorean Triangle

Let $a$ and $b$ be the legs of a Pythagorean triangle $P_1$.
Let $\tuple {a, b}$ be used as the generator for a new Pythagorean triangle $P_2$.
Then the hypotenuse of $P_2$ is the square of the hypotenuse of $P_1$.

Proof:
By Pythagoras's Theorem, the square of the hypotenuse of $P_1$ is $a^2 + b^2$.
By Solutions of Pythagorean Equation, the sides of $P_2$ can be expressed as $\tuple {2 a b, a^2 - b^2, a^2 + b^2}$, where the hypotenuse is $a^2 + b^2$.
{{qed}}
Theorem: Rational Number plus Irrational Number is Irrational

Rational number plus irrational number is irrational.
That is, let $x \in \Q$, $y \in \R \setminus \Q$ and $x + y = z$.
Then $z \in \R \setminus \Q$.

Proof:
{{AimForCont}} $z \in \Q$.
By definition of rational numbers:
:$\exists a, b \in \Z, b \ne 0: x = \dfrac a b$
:$\exists c, d \in \Z, d \ne 0: z = \dfrac c d$
Then:
{{begin-eqn}}
{{eqn | l = x + y
      | r = z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac a b + y
      | r = \dfrac c d
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \dfrac {b c - a d} {b d}
      | c = by rearrangement
}}
{{end-eqn}}
This shows that $y$ is  rational, which is a contradiction.
By Proof by Contradiction, $z$ is irrational.
{{qed}}
Category:Rational Numbers
Category:Irrational Numbers
oewkqy1szldvm50y77fqhvs2pevj8ei
Theorem: Simple Variable End Point Problem/Endpoints on Curves

Let $y$, $F$, $\phi$ and $\psi$ be smooth real functions.
Let $J = J \sqbrk y$ be a functional of the form:
:$\ds J \sqbrk y = \int_{x_0}^{x_1} \map F {x, y, y'} \rd x$
Let $P_0$, $P_1$ be the endpoints of the curve $y$.
Suppose $P_0$, $P_1$ lie on curves $y = \map {\phi} x$, $y = \map {\psi} x$.
Then the extremum of $J \sqbrk y$ is a curve which satisfies the following system of Euler and transversality equations:
{{begin-eqn}}
{{eqn | l = F_y - \dfrac \d {\d x} F_{y'}
      | r = 0
}}
{{eqn | l = \bigvalueat {\paren {F + \paren {\phi' - y'} F_{y'} } } {x \mathop = x_0}
      | r = 0
}}
{{eqn | l = \bigvalueat {\paren {F + \paren {\psi' - y'} F_{y'} } } {x \mathop = x_1} = 0
      | r = 0
}}
{{end-eqn}}
{{explain|meaning of square brackets}}

Proof:
By general variation of integral functional with $n = 1$:
:$\ds \delta J \sqbrk{y; h} = \int_{x_0}^{x_1} \intlimits {\paren {F_y - \dfrac \d {\d x} F_{y'} } \map h x + F_{y'} \delta y} {x \mathop = x_0} {x \mathop = x_1} + \bigintlimits {\paren {F - y'F_{y'} } \delta x} {x \mathop = x_0} {x \mathop = x_1}$
Since the curve $y = \map y x$ is an extremum of $\map J y$, the integral term vanishes:
:$\ds \delta J \sqbrk {y; h} = \bigintlimits {F_{y'} \delta y} {x \mathop = x_0} {x \mathop = x_1} + \bigintlimits {\paren {F - y'F_{y'} } \delta x} {x \mathop = x_0} {x \mathop = x_1}$
According to Taylor's Theorem:
:$\delta y_0 = \paren {\map {\phi'} {x_0} + \epsilon_0} \delta x_0$
:$\delta y_1 = \paren {\map {\phi'} {x_1} + \epsilon_1} \delta x_1$
where $\epsilon_0 \to 0$ as $\delta x_0 \to 0$ and $\epsilon_1 \to 0$ as $\delta x_1 \to 0$.
{{Stub| add a figure; explain better}}
Substitution of $\delta y_0$ and $\delta y_1$ into $\delta J$ leads to:
:$\delta J \sqbrk {y; h} = \bigvalueat {\paren {F_{y'} \psi' + F - y' F_{y'} } } {x \mathop = x_1} \delta x_1 - \bigvalueat {\paren {F_{y'} \psi' + F - y' F_{y'} } } {x \mathop = x_0} \delta x_0$
$y = \map y x$ is an extremal of $J \sqbrk y$, thus $\delta J = 0$.
$\delta x_0$ and $\delta x_1$ are independent increments. 
Hence both remaining terms in $\delta J$ vanish independently.
{{qed}}
Theorem: Lower Closure of Element is Topologically Closed in Scott Topological Ordered Set

Let $\struct {S, \preceq}$ be an up-complete ordered set.
Let $T = \struct {S, \preceq, \tau}$ be a relational structure with the Scott topology.
Let $x \in S$.
Let $x^\preceq$ denote the lower closure of $x$.
Then $x^\preceq$ is topologically closed.

Proof:
By Lower Closure of Element is Closed under Directed Suprema:
:$x^\preceq$ is closed under directed suprema.
By Lower Closure of Singleton:
:$\set x^\preceq = x^\preceq$
By Lower Closure is Lower Section:
:$x^\preceq$ is a lower section.
Thus by Closed Set iff Lower and Closed under Directed Suprema in Scott Topological Ordered Set:
:$x^\preceq$ is closed.
{{qed}}
Theorem: Complement of Lower Closure of Element is Open in Scott Topological Ordered Set

Let $T = \struct {S, \preceq, \tau}$ be a relational structure with Scott topology
where $\struct {S, \preceq}$ is an up-complete ordered set.
Let $x \in S$.
Then $\relcomp S {x^\preceq}$ is topologically open,
where
:$x^\preceq$ denotes the lower closure of $x$,
:$\relcomp S {x^\preceq}$ denotes the relative complement of $x^\preceq$.

Proof:
By Lower Closure of Element is Topologically Closed in Scott Topological Ordered Set:
:$x^\preceq$ is closed.
By definition of closed set:
:$\relcomp S {x^\preceq} \in \tau$
Thus by definition:
:$\relcomp S {x^\preceq}$ is a open set.
{{qed}}
Theorem: Open iff Upper and with Property (S) in Scott Topological Lattice

Let $T = \struct {S, \preceq, \tau}$ be an up-complete topological lattice.
Let $A$ be a subset of $S$.
Then $A$ is open {{iff}} $A$ is upper and with property (S).

Proof:
=== Sufficient Condition ===
Let $A$ be open.
Thus by definition of Scott topology:
:$A$ is an upper section.
Let $D$ be a directed subset of $S$ such that
:$\sup D \in A$
By definition of Scott topology:
:$A$ is inaccessible by directed suprema.
By definition of inaccessible by directed suprema:
:$A \cap D \ne \O$
By definition of non-empty:
:$\exists y: y \in A \cap D$
By definition of intersection:
:$y \in A$ and $y \in D$
Thus $y \in D$.
Thus by definition of upper section:
:$\forall x \in D: y \preceq x \implies x \in A$
{{qed|lemma}}
Theorem: Euler's Equation for Vanishing Variation in Canonical Variables

{{refactor|There are a number of pages linking here with the presentation of the link set as "momenta". This is going to need a definition of its own, but it is not clear what that is from looking at this page.|level = advanced}}
Consider the following system of differential equations:
:<nowiki>$(1): \quad \begin {cases} F_{y_i} - \dfrac \d {\d x} F_{y_i'} = 0 \\
\dfrac {\d {y_i} } {\d x} = y_i'\end{cases}$</nowiki>
where $i \in \set {1, \ldots, n}$.
Let the coordinates $\tuple {x, \family {y_i}_{1 \mathop \le i \mathop \le n}, \family {y_i'}_{1 \mathop \le i \mathop \le n}, F}$ be transformed to canonical variables:
:$\tuple {x, \family {y_i}_{1 \mathop \le i \mathop \le n}, \family {p_i}_{1 \mathop \le i \mathop \le n}, H}$
Then the system $(1)$ is transformed into:
:<nowiki>$\begin {cases}
\dfrac {\d y_i} {\d x} = \dfrac {\partial H} {\partial p_i} \\
\dfrac {\d p_i} {\d x} = -\dfrac {\partial H} {\partial y_i}
\end {cases}$</nowiki>

Proof:
Find the full differential of Hamiltonian:
{{begin-eqn}}
{{eqn | l = \rd H
      | r = -\rd F + \rd {\sum_{i \mathop = 1}^n y_i' p_i}
      | c = {{Defof|Hamiltonian}}
}}
{{eqn | r = -\rd F + \sum_{i \mathop = 1}^n \paren {\rd {y_i'} p_i + y_i' \rd p_i}
      | c = Full differential of a product
}}
{{eqn | r = -\frac {\partial F} {\partial x} \rd x - \sum_{i \mathop = 1}^n \frac {\partial F} {\partial y_i} \rd y_i - \sum_{i \mathop = 1}^n \frac {\partial F} {\partial y_i'} \rd y_i' + {\sum_{i \mathop = 1}^n \rd y_i' p_i} + \sum_{i \mathop = 1}^n y_i'\rd p_i
      | c = {{Defof|Differential of Real-Valued Function}}
}}
{{eqn | r = -\frac {\partial F} {\partial x} \rd x - \sum_{i \mathop = 1}^n \frac {\partial F} {\partial y_i} \rd y_i - \sum_{i \mathop = 1}^n p_i \rd y_i' + {\sum_{i \mathop = 1}^n \rd y_i' p_i} + \sum_{i \mathop = 1}^n y_i'\rd p_i
      | c = {{Defof|Canonical Variable}}: $p_i$
}}
{{eqn | r = -\frac {\partial F} {\partial x} \rd x - \sum_{i \mathop = 1}^n \frac {\partial F} {\partial y_i} \rd y_i + \sum_{i \mathop = 1}^n y_i' \rd p_i
      | c = Terms with $p_i \rd y_i'$ cancel 
}}
{{eqn | r = \frac {\partial H} {\partial x} \rd x + \sum_{i \mathop = 1}^n \frac {\partial H} {\partial y_i} \rd y_i + \sum_{i \mathop = 1}^n \frac {\partial H} {\partial p_i} \rd p_i
      | c = {{Defof|Differential of Real-Valued Function}}
}}
{{end-eqn}}
By equating coefficients of differentials in last two equations we find that:
:$\dfrac {\partial H} {\partial x} = -\dfrac {\partial F} {\partial x}$
:$\dfrac {\partial H} {\partial y_i} = -\dfrac {\partial F} {\partial y_i}$
:$\dfrac {\partial H} {\partial p_i} = y_i'$
From the third identity it follows that:
:$\paren {\dfrac {\d y_i} {\d x} = y_i} \implies \paren {\dfrac {\d y_i} {\d x} = \dfrac {\partial H} {\partial p_i} }$
while the second identity together with the definition of $p_i$ assures that:
:$\paren {\dfrac {\partial F} {\partial y_i} - \dfrac \d {\d x} \dfrac {\partial F} {\partial y_i} = 0} \implies \paren {\dfrac {\d p_i} {\d x} = -\dfrac {\partial H} {\partial y_i} }$
{{qed}}
{{Namedfor|Leonhard Paul Euler|cat = Euler}}
Theorem: Relational Structure with Topology of Subsets with Property (S) is Topological Space

Let $T = \struct {S, \preceq, \tau}$ be a relational structure with topology
where
:$\struct {S, \preceq}$ is an up-complete ordered set
:$\tau$ is the set of all subsets of $S$ with property (S).
Then $\struct {S, \tau}$ is topological space.

Proof:
We will prove that
:$S$ has property (S).
Let $D$ be a directed subset of $S$ such that
:$\sup D \in S$
By definition of non-empty set:
:$\exists y: y \in D$
Thus $y \in D$.
Thus by definition of subset:
:$\forall x \in D: y \preceq x \implies x \in S$
{{qed|lemma}}
Then:
$(\text O 3): \quad S \in \tau$
We will prove that:
:$(\text O 1): \quad \forall F \subseteq \tau: \bigcup F \in \tau$
Let $F \subseteq \tau$.
To prove that $\bigcup F \in \tau$ it should be proved that
:$\bigcup F$ has property (S).
Let $D$ be a directed subset of $S$ such that
:$\sup D \in \bigcup F$
By definition of union:
:$\exists X \in F: \sup D \in X$
By definition of subset:
:$X \in \tau$
By assumption:
:$X$ has property (S).
By definition of property (S):
:$\exists y \in D: \forall x \in D: y \preceq x \implies x \in X$
Thus $y \in D$.
Let $x \in D$ such that
:$y \preceq x$
Then $x \in X$.
Thus by definition of union:
:$x \in \bigcup F$
{{qed|lemma}}
We will prove that
:$(\text O 2): \quad \forall X, Y \in \tau: X \cap Y \in \tau$
Let $X, Y \in \tau$.
By assumption:
:$X$ and $Y$ have property (S).
To prove that $X \cap Y \in \tau$ it should be proved that:
:$X \cap Y$ has property (S).
Let $D$ be a directed subset of $S$ such that:
:$\sup D \in X \cap Y$
By definition of intersection:
:$\sup D \in X$ and $\sup D \in Y$
By definition of property (S):
:$\exists x \in D: \forall z \in D: x \preceq z \implies z \in X$
and
:$\exists y \in D: \forall z \in D: y \preceq z \implies z \in X$
By definition of directed:
:$\exists z \in D: x \preceq z \land y \preceq z$
Thus $z \in D$.
Let $u \in D$ such that
:$z \preceq u$
By definition of transitivity:
:$x \preceq u$ and $y \preceq u$
Then:
:$u \in X$ and $u \in Y$
Thus by definition of intersection:
:$u \in X \cap Y$
{{qed|lemma}}
Hence by $(\text O 1)$, $(\text O 2)$, $(\text O 3)$, and definition:
:$\struct {S, \tau}$ is topological space.
{{qed}}