avewright/proofwiki-math huggingface dataset:
Theorem: Ordinals are Well-Ordered

The ordinals are well-ordered.

Proof:
Recall that the Ordinals are Totally Ordered.
Let $A$ be a non-empty set of ordinals.
Let $\alpha \in A$.
Let $B = \alpha^+ \cap A$, where $\alpha^+$ denotes the successor set of $\alpha$.
Recall that $\alpha^+$ is an ordinal.
Note that $\alpha \in B$, so $B$ is non-empty.
By Intersection is Subset, $B \subseteq \alpha^+$.
It follows that there exists a smallest element $\kappa$ of $B$.
We claim that $\kappa$ is the smallest element of $A$.
So let $\beta \in A$. We need to show that $\kappa = \beta$ or $\kappa \in \beta$.
By Ordinal Membership is Trichotomy, either $\beta \in \alpha^+$, $\alpha^+ = \beta$, or $\alpha^+ \in \beta$.
If $\beta \in \alpha^+$, then $\beta \in B$; it follows by the definition of $\kappa$ that $\kappa = \beta$ or $\kappa \in \beta$.
If $\alpha^+ = \beta$ or $\alpha^+ \in \beta$, then it follows by the transitivity of $\beta$ that $\alpha^+ \subseteq \beta$.
Since $\kappa \in \alpha^+$, it follows that $\kappa \in \beta$.
{{qed}}
Theorem: Ordinals are Well-Ordered

The ordinals are well-ordered.

Proof:
By Ordinals are Totally Ordered, the ordinals are totally ordered by $\subseteq$:
{{begin-eqn}}
{{eqn | l = X
      | o = \subsetneqq
      | r = Y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists a \in Y
      | l = X
      | r = Y_a
      | c = where $Y_a$ denotes the initial segment of $Y$ determined by $a$
}}
{{eqn | ll= \leadstoandfrom
      | l = X
      | r = a
      | c = since $Y_a = a$
}}
{{eqn | ll= \leadstoandfrom
      | l = X
      | o = \in
      | r = Y
      | c = 
}}
{{end-eqn}}
Thus:
:the strict ordering $\subsetneqq$ on ordinals
and
:the strict ordering $\in$ on ordinals
are the same.
{{AimForCont}} the ordinals were not well-ordered by $\subsetneqq$.
Then we could find a sequence $\sequence {X_n}_{n \mathop = 0}^\infty$ of ordinals such that:
:$X_0 \supsetneqq X_1 \supsetneqq X_2 \cdots$
So for all $n > 0$:
:$X_n \subsetneqq X_0$
so:
:$X_n \in X_0$
Thus $\sequence {X_{n + 1} }_{n \mathop = 0}^\infty$ is a decreasing sequence under $\subsetneqq$ of elements of $\sequence {X_n}$.
But since $X_0$ is an ordinal it is well-ordered by $\subsetneqq$.
From Infinite Sequence Property of Well-Founded Relation, this demonstrates a contradiction.
{{qed}}
Theorem: Set Intersection Preserves Subsets/Corollary/Proof 1

Let $A, B, S$ be sets.
Then:
:$A \subseteq B \implies A \cap S \subseteq B \cap S$

Proof:
Let $A \subseteq B$, and let $S$ be any set.
From Set Intersection Preserves Subsets:
:$A \subseteq B, \ S \subseteq T \implies A \cap S \subseteq B \cap T$
for arbitrary sets $S$ and $T$.
Substituting $S$ for $T$:
:$A \subseteq B, \ S \subseteq S \implies A \cap S \subseteq B \cap S$
From Set is Subset of Itself, $S \subseteq S$ for all sets $S$.
Hence the result:
:$A \subseteq B \implies A \cap S \subseteq B \cap S$
{{qed}}
Theorem: Set Intersection Preserves Subsets/Corollary

Let $A, B, S$ be sets.
Then:
:$A \subseteq B \implies A \cap S \subseteq B \cap S$

Proof:
Let $A \subseteq B$, and let $S$ be any set.
From Set Intersection Preserves Subsets:
:$A \subseteq B, \ S \subseteq T \implies A \cap S \subseteq B \cap T$
for arbitrary sets $S$ and $T$.
Substituting $S$ for $T$:
:$A \subseteq B, \ S \subseteq S \implies A \cap S \subseteq B \cap S$
From Set is Subset of Itself, $S \subseteq S$ for all sets $S$.
Hence the result:
:$A \subseteq B \implies A \cap S \subseteq B \cap S$
{{qed}}
Theorem: Set Intersection Preserves Subsets/Corollary

Let $A, B, S$ be sets.
Then:
:$A \subseteq B \implies A \cap S \subseteq B \cap S$

Proof:
Recall the Factor Principles, themselves a corollary of the Praeclarum Theorema:
:$\paren {p \implies q} \vdash \paren {p \land r} \implies \paren {q \land r}$
This is applied as:
{{begin-eqn}}
{{eqn | o = 
      | r = A \subseteq B
      | c = 
}}
{{eqn | o = \leadsto
      | r = \paren {x \in A \implies x \in B}
      | c = {{Defof|Subset}}
}}
{{eqn | o = \leadsto
      | r = \paren {x \in A \land x \in S \implies x \in B \land x \in S}
      | c = Factor Principles
}}
{{eqn | o = \leadsto
      | r = \paren {x \in A \cap S \implies x \in B \cap S}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = A \cap S \subseteq B \cap S
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
{{Qed}}
Theorem: Set Intersection Preserves Subsets/Families of Sets/Corollary

Let $I$ be an indexing set.
Let $\family {B_\alpha}_{\alpha \mathop \in I}$ be an indexed family of subsets of a set $S$.
Let $A$ be a set such that $A \subseteq B_\alpha$ for all $\alpha \in I$.
Then:
:$\ds A \subseteq \bigcap_{\alpha \mathop \in I} B_\alpha$

Proof:
For each $\alpha \in I$, define $A_\alpha := A$.
Then by Set Intersection is Idempotent, it follows that:
:$\ds \bigcap_{\alpha \mathop \in I} A_\alpha = A$
Since $A \subseteq B_\alpha$ for all $\alpha \in I$, the premises of Set Intersection Preserves Subsets are satisfied.
Applying this theorem gives:
:$\ds A = \bigcap_{\alpha \mathop \in I} A_\alpha \subseteq \bigcap_{\alpha \mathop \in I} B_\alpha$
which is precisely the desired result.
{{qed}}
Category:Set Intersection Preserves Subsets
Category:Indexed Families
qoqljj3t1qqohxabdjrgwpobzsxajn4
Theorem: Intersection is Largest Subset/General Result

Let $T$ be a set.
Let $\powerset T$ be the power set of $T$.
Let $\mathbb T$ be a subset of $\powerset T$.
Then:
:$\paren {\forall X \in \mathbb T: S \subseteq X} \iff S \subseteq \bigcap \mathbb T$
=== Family of Sets ===
In the context of a family of sets, the result can be presented as follows:
{{:Intersection is Largest Subset/Family of Sets}}

Proof:
Let $\mathbb T \subseteq \powerset T$.
Suppose that $\forall X \in \mathbb T: S \subseteq X$.
Consider any $x \in S$.
By definition of subset, it follows that:
:$\forall X \in \mathbb T: x \in X$
Thus it follows from definition of set intersection that:
:$x \in \bigcap \mathbb T$
Thus by definition of subset, it follows that:
:$S \subseteq \bigcap \mathbb T$
So:
:$\paren {\forall X \in \mathbb T: S \subseteq X} \implies S \subseteq \bigcap \mathbb T$
{{qed|lemma}}
Now suppose that $S \subseteq \bigcap \mathbb T$.
From Intersection is Subset: General Result we have:
:$\forall X \in \mathbb T: \bigcap \mathbb T \subseteq X$
So from Subset Relation is Transitive, it follows that:
:$\forall X \in \mathbb T: S \subseteq \bigcap \mathbb T \subseteq X$
So it follows that $\forall X \in \mathbb T: S \subseteq X$.
So:
:$S \subseteq \bigcap \mathbb T \implies \paren {\forall X \in \mathbb T: S \subseteq X}$
{{qed|lemma}}
Hence:
:$\paren {\forall X \in \mathbb T: S \subseteq X} \iff S \subseteq \bigcap \mathbb T$
{{Qed}}
Theorem: Union is Smallest Superset/General Result

Let $S$ and $T$ be sets.
Let $\powerset S$ denote the power set of $S$.
Let $\mathbb S$ be a subset of $\powerset S$.
Then:
:$\ds \paren {\forall X \in \mathbb S: X \subseteq T} \iff \bigcup \mathbb S \subseteq T$
=== Family of Sets ===
In the context of a family of sets, the result can be presented as follows:
{{:Union is Smallest Superset/Family of Sets}}

Proof:
Let $\mathbb S \subseteq \powerset S$.
By Union of Subsets is Subset: Subset of Power Set:
:$\ds \paren {\forall X \in \mathbb S: X \subseteq T} \implies \bigcup \mathbb S \subseteq T$
{{qed|lemma}}
Now suppose that $\ds \bigcup \mathbb S \subseteq T$.
Consider any $X \in \mathbb S$ and take any $x \in X$.
From Set is Subset of Union: General Result we have that:
:$\ds X \subseteq \bigcup \mathbb S$
Thus:
:$\ds x \in \bigcup \mathbb S$
But:
:$\ds \bigcup \mathbb S \subseteq T$
So it follows that:
:$X \subseteq T$
So:
:$\ds \bigcup \mathbb S \subseteq T \implies \paren {\forall X \in \mathbb S: X \subseteq T}$
{{qed|lemma}}
Hence:
:$\ds \paren {\forall X \in \mathbb S: X \subseteq T} \iff \bigcup \mathbb S \subseteq T$
{{Qed}}
Theorem: Mapping is Involution iff Bijective and Symmetric

Let $S$ be a set.
Let $f: S \to S$ be a mapping on $S$.
Then $f$ is an involution {{iff}} $f$ is both a bijection and a symmetric relation.

Proof:
By definition an involution on $S$ is a mapping such that:
:$\forall x \in S: \map f {\map f x} = x$
Theorem: Cardinality of Set Union/Corollary

Let $S_1, S_2, \ldots, S_n$ be finite sets which are pairwise disjoint.
Then:
:$\ds \card {\bigcup_{i \mathop = 1}^n S_i} = \sum_{i \mathop = 1}^n \card {S_i}$
Specifically:
:$\card {S_1 \cup S_2} = \card {S_1} + \card {S_2}$

Proof:
As $S_1, S_2, \ldots, S_n$ are pairwise disjoint, their intersections are all empty.
The Cardinality of Set Union holds, but from Cardinality of Empty Set, all the terms apart from the first vanish.
{{qed}}
Theorem: Cartesian Product of Preimage with Image of Relation is Correspondence

Let $\RR \subseteq S \times T$ be a relation.
Then the restriction of $\RR$ to $\Preimg \RR \times \Img \RR$ is a correspondence.

Proof:
By the definition of a correspondence it will be shown that $\RR$ is both left-total and right-total.
$\RR$ is left-total {{iff}}:
:$\forall x \in S: \exists y \in T: x \mathrel \RR y$
By the definition of the pre-image of $\RR$:
:$\Preimg \RR = \set {x \in S: \exists y \in T: x \mathrel \RR y}$
Therefore $\RR$ is left-total.
$\RR$ is right-total {{iff}}:
:$\forall x \in T: \exists y \in S: x \mathrel \RR y$
By the definition of the image of $\RR$:
:$\Img \RR = \set {x \in T: \exists y \in S: x \mathrel \RR y}$
Therefore $\RR$ is right-total.
Hence $\RR$ is a correspondence.
{{qed}}
Category:Relation Theory
t1okmpbvf8bddrihngxobt45w20fpvm
Theorem: Image of Intersection under Relation/General Result

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation.
Let $\powerset S$ be the power set of $S$.
Let $\mathbb S \subseteq \powerset S$.
Then:
:$\ds \RR \sqbrk {\bigcap \mathbb S} \subseteq \bigcap_{X \mathop \in \mathbb S} \RR \sqbrk X$

Proof:
{{begin-eqn}}
{{eqn | q = \forall X \in \mathbb S
      | l = \bigcap \mathbb S
      | o = \subseteq
      | r = X
      | c = Intersection is Subset: General Result
}}
{{eqn | ll= \leadsto
      | q = \forall X \in \mathbb S
      | l = \RR \sqbrk {\bigcap \mathbb S}
      | o = \subseteq
      | r = \RR \sqbrk X
      | c = Image of Subset is Subset of Image
}}
{{eqn | ll= \leadsto
      | l = \RR \sqbrk {\bigcap \mathbb S}
      | o = \subseteq
      | r = \bigcap_{X \mathop \in \mathbb S} \RR \sqbrk X
      | c = Intersection is Largest Subset: General Result
}}
{{end-eqn}}
{{qed}}
Category:Image of Intersection under Relation
44wo28tv3erq7w3e3qtv3vdx6ovjmsn
Theorem: Image of Intersection under One-to-Many Relation/General Result

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation.
Let $\powerset S$ be the power set of $S$.
Then:
:$\ds \forall \mathbb S \subseteq \powerset S: \RR \sqbrk {\bigcap \mathbb S} = \bigcap_{X \mathop \in \mathbb S} \RR \sqbrk X$ 
{{iff}} $\RR$ is one-to-many.

Proof:
=== Sufficient Condition ===
Suppose:
:$\ds \RR \sqbrk {\bigcap \mathbb S} = \bigcap_{X \mathop \in \mathbb S} \RR \sqbrk X$ 
where $\mathbb S$ is ''any'' subset of $\powerset S$.
Then by definition of $\mathbb S$:
:$\forall S_1, S_2 \in \mathbb S: \RR \sqbrk {S_1 \cap S_2} = \RR \sqbrk {S_1} \cap \RR \sqbrk {S_2}$
and the sufficient condition applies for Image of Intersection under One-to-Many Relation.
So $\RR$ is one-to-many.
{{qed|lemma}}
Theorem: Image of Union under Relation/General Result

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation.
Let $\powerset S$ be the power set of $S$.
Let $\mathbb S \subseteq \powerset S$.
Then:
:$\ds \RR \sqbrk {\bigcup \mathbb S} = \bigcup_{X \mathop \in \mathbb S} \RR \sqbrk X$

Proof:
{{begin-eqn}}
{{eqn | l = t
      | o = \in
      | r = \RR \sqbrk {\bigcup \mathbb S}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists s \in \bigcup \mathbb S
      | l = t
      | o = \in
      | r = \map \RR s
      | c = Image of Subset under Relation equals Union of Images of Elements
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists X \in \mathbb S: \exists s \in X
      | l = t
      | o = \in
      | r = \map \RR s
      | c = {{Defof|Union of Set of Sets}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists X \in \mathbb S
      | l = t
      | o = \in
      | r = \RR \sqbrk X
      | c = {{Defof|Image of Subset under Relation}}
}}
{{eqn | ll= \leadstoandfrom
      | l = t
      | o = \in
      | r = \bigcup_{X \mathop \in \mathbb S} \RR \sqbrk X
      | c = {{Defof|Union of Set of Sets}}
}}
{{end-eqn}}
{{Qed}}
Category:Image of Union under Relation
ciwalubgs46tx1t75idbnowhvtff958
Theorem: Image of Union under Mapping/General Result

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let $\powerset S$ be the power set of $S$.
Let $\mathbb S \subseteq \powerset S$.
Then:
:$\ds f \sqbrk {\bigcup \mathbb S} = \bigcup_{X \mathop \in \mathbb S} f \sqbrk X$
This can be expressed in the language and notation of direct image mappings as:
:$\ds \forall \mathbb S \subseteq \powerset S : \map {f^\to} {\bigcup \mathbb S} = \bigcup_{X \mathop \in \mathbb S} \map {f^\to} X$

Proof:
As $f$, being a mapping, is also a relation, we can apply Image of Union under Relation: General Result:
:$\ds \RR \sqbrk {\bigcup \mathbb S} = \bigcup_{X \mathop \in \mathbb S} \RR \sqbrk X$
{{qed}}
Theorem: Preimage of Union under Mapping/General Result

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let $\powerset T$ be the power set of $T$.
Let $\mathbb T \subseteq \powerset T$.
Then:
:$\ds f^{-1} \sqbrk {\bigcup \mathbb T} = \bigcup_{X \mathop \in \mathbb T} f^{-1} \sqbrk X$

Proof:
As $f$, being a mapping, is also a relation, we can apply Preimage of Union under Relation: General Result:
:$\ds \RR^{-1} \sqbrk {\bigcup \mathbb T} = \bigcup_{X \mathop \in \mathbb T} \RR^{-1} \sqbrk X$
{{qed}}
Theorem: Preimage of Union under Relation/General Result

Let $S$ and $T$ be sets.
Let $\RR \subseteq S \times T$ be a relation.
Let $\powerset T$ be the power set of $T$.
Let $\mathbb T \subseteq \powerset T$.
Then:
:$\ds \RR^{-1} \sqbrk {\bigcup \mathbb T} = \bigcup_{X \mathop \in \mathbb T} \RR^{-1} \sqbrk X$
where $\RR^{-1} \sqbrk X$ denotes the preimage of $X$ under $\RR$.

Proof:
We have that $\RR^{-1}$ is a relation.
The result follows from Image of Union under Relation: General Result.
{{qed}}
Category:Preimage of Union under Relation
16qvgywv4ku7oc1lyi9d44gxd95zlxw
Theorem: Image of Intersection under Mapping/General Result

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let $\powerset S$ be the power set of $S$.
Let $\mathbb S \subseteq \powerset S$.
Then:
:$\ds f \sqbrk {\bigcap \mathbb S} \subseteq \bigcap_{X \mathop \in \mathbb S} f \sqbrk X$

Proof:
As $f$, being a mapping, is also a relation, we can apply Image of Intersection under Relation: General Result:
:$\ds \RR \sqbrk {\bigcap \mathbb S} \subseteq \bigcap_{X \mathop \in \mathbb S} \RR \sqbrk X$
{{qed}}
Theorem: Preimage of Intersection under Mapping/General Result

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let $\powerset T$ be the power set of $T$.
Let $\mathbb T \subseteq \powerset T$.
Then:
:$\ds f^{-1} \sqbrk {\bigcap \mathbb T} = \bigcap_{X \mathop \in \mathbb T} f^{-1} \sqbrk X$

Proof:
$f$ is a mapping.
Therefore it is by definition a many-to-one relation.
It follows from Inverse of Many-to-One Relation is One-to-Many that its inverse $f^{-1}$ is a one-to-many relation.
Thus Image of Intersection under One-to-Many Relation: General Result applies:
:$\ds \RR \sqbrk {\bigcap \mathbb T} = \bigcap_{X \mathop \in \mathbb T} \RR \sqbrk X$
where here $\RR = f^{-1}$.
{{Qed}}
Theorem: Bijective Relation has Left and Right Inverse

Let $\RR \subseteq S \times T$ be a relation on a cartesian product $S \times T$.
Let:
:$I_S$ be the identity mapping on $S$
:$I_T$ be the identity mapping on $T$.
Let $\RR^{-1}$ be the inverse relation of $\RR$.
Let $\RR$ be a bijection.
Then:
:$\RR^{-1} \circ \RR = I_S$
and
:$\RR \circ \RR^{-1} = I_T$
where $\circ$ denotes composition of relations.

Proof:
Suppose $\RR$ is a bijection.
Then by definition:
:$(1): \quad \RR$ is a surjection and therefore right-total.
:$(2): \quad \RR$ is a mapping and therefore left-total.
:$(3): \quad \RR$ is a one-to-one relation and therefore also both a many-to-one relation and a one-to-many relation.
By Inverses of Right-Total and Left-Total Relations, we have that $\RR^{-1}$ is also both right-total and left-total.
By Inverse of Many-to-One Relation is One-to-Many we have that $\RR^{-1}$ is also both a many-to-one relation and a one-to-many relation.
From Condition for Composite Relation with Inverse to be Identity, it follows that:
:$\RR^{-1} \circ \RR = I_S$
and:
:$\RR \circ \RR^{-1} = I_T$
Hence the result.
{{qed}}
Theorem: Left and Right Inverse Relations Implies Bijection

Let $\RR \subseteq S \times T$ be a relation on a cartesian product $S \times T$.
Let:
:$I_S$ be the identity mapping on $S$
:$I_T$ be the identity mapping on $T$.
Let $\RR^{-1}$ be the inverse relation of $\RR$.
Let $\RR$ be such that:
:$\RR^{-1} \circ \RR = I_S$ and
:$\RR \circ \RR^{-1} = I_T$
where $\circ$ denotes composition of relations.
Then $\RR$ is a bijection.

Proof:
Let $\RR \subseteq S \times T$ be such that:
:$\RR^{-1} \circ \RR = I_S$
and:
:$\RR \circ \RR^{-1} = I_T$.
From Condition for Composite Relation with Inverse to be Identity, we have that:
:$\RR$ is many-to-one
:$\RR$ is right-total
:$\RR^{-1}$ is many-to-one
:$\RR^{-1}$ is right-total.
From Inverse of Many-to-One Relation is One-to-Many, it follows that both $\RR$ and $\RR^{-1}$ are by definition one-to-one.
From Inverses of Right-Total and Left-Total Relations, it also follows that both $\RR$ and $\RR^{-1}$ are left-total.
By definition, an injection is a relation which is:
:One-to-one
:left-total.
Also by definition, a surjection is a relation which is:
:Left-total
:Many-to-one
:Right-total.
It follows that $\RR$ is both an injection and a surjection, and so by definition a bijection.
By the same coin, the same applies to $\RR^{-1}$.
{{qed}}
Theorem: Bijection has Left and Right Inverse

Let $f: S \to T$ be a bijection.
Let:
: $I_S$ be the identity mapping on $S$
: $I_T$ be the identity mapping on $T$.
Let $f^{-1}$ be the inverse of $f$.
Then:
: $f^{-1} \circ f = I_S$
and:
: $f \circ f^{-1} = I_T$
where $\circ$ denotes composition of mappings.

Proof:
Let $f$ be a bijection.
Then it is both an injection and a surjection, thus both the described $g_1$ and $g_2$ must exist from Injection iff Left Inverse and Surjection iff Right Inverse.
The fact that $g_1 = g_2 = f^{-1}$ follows from Left and Right Inverses of Mapping are Inverse Mapping.
{{qed}}
Theorem: Bijection has Left and Right Inverse

Let $f: S \to T$ be a bijection.
Let:
: $I_S$ be the identity mapping on $S$
: $I_T$ be the identity mapping on $T$.
Let $f^{-1}$ be the inverse of $f$.
Then:
: $f^{-1} \circ f = I_S$
and:
: $f \circ f^{-1} = I_T$
where $\circ$ denotes composition of mappings.

Proof:
Suppose $f$ is a bijection.
From Bijection iff Inverse is Bijection and Composite of Bijection with Inverse is Identity Mapping, it is shown that the inverse mapping $f^{-1}$ such that:
: $f^{-1} \circ f = I_S$
: $f \circ f^{-1} = I_T$
is a bijection.
{{qed}}
Theorem: Bijection has Left and Right Inverse

Let $f: S \to T$ be a bijection.
Let:
: $I_S$ be the identity mapping on $S$
: $I_T$ be the identity mapping on $T$.
Let $f^{-1}$ be the inverse of $f$.
Then:
: $f^{-1} \circ f = I_S$
and:
: $f \circ f^{-1} = I_T$
where $\circ$ denotes composition of mappings.

Proof:
Let $f$ be a bijection.
By definition, $f$ is a mapping, and hence also by definition a relation.
Hence the result Bijective Relation has Left and Right Inverse applies directly and so:
:$f^{-1} \circ f = I_S$
and
:$f \circ f^{-1} = I_T$
{{qed}}
Theorem: Symmetry in Space Implies Conservation of Momentum

The total derivative of the action $S_{12}$ from states $1$ to $2$ with regard to position is equal to the difference in momentum from states $1$ to $2$:
:$\dfrac {\d S_{1 2} } {\d x} = p_2 - p_1$

Proof:
From the definition of generalized momentum and the Euler-Lagrange Equations:
{{begin-eqn}}
{{eqn | l = 0
      | r = \frac \d {\d t} \frac {\partial \LL} {\partial \dot x} - \frac {\partial \LL} {\partial x}
      | c = 
}}
{{eqn | r = \dot p_i - \frac {\partial \LL} {\partial x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dot p_i
      | r = \frac {\partial \LL} {\partial x}
      | c =  
}}
{{end-eqn}}
Therefore, via the definition of action, Definite Integral of Partial Derivative and the Fundamental Theorem of Calculus:
{{begin-eqn}}
{{eqn | l = \frac {\d S_{12} } {\d x}
      | r = \frac \d {\d x} \int_{t_1}^{t_2} \LL \rd t
      | c = 
}}
{{eqn | r = \int_{t_1}^{t_2} \frac {\partial \LL} {\partial x} \rd t
      | c = 
}}
{{eqn | r = \int_{t_1}^{t_2} \dot p_i \rd t
      | c = 
}}
{{eqn | r = p_2 - p_1
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Laws of Conservation
2gn1loqtdl26f41duyeoay3fyrds0cs
Theorem: Image of Intersection under Injection/General Result

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Let $\powerset S$ be the power set of $S$.
Then:
:$\ds \forall \mathbb S \subseteq \powerset S: f \sqbrk {\bigcap \mathbb S} = \bigcap_{X \mathop \in \mathbb S} f \sqbrk X$ 
{{iff}} $f$ is an injection.
This can be expressed in the language and notation of direct image mappings as:
:$\ds \forall \mathbb S \subseteq \powerset S : \map {f^\to} {\bigcap \mathbb S} = \bigcap_{X \mathop \in \mathbb S} \map {f^\to} X$

Proof:
An injection is a type of one-to-one relation, and therefore also a one-to-many relation.
Therefore Image of Intersection under One-to-Many Relation applies:
:$\ds \forall \mathbb S \subseteq \powerset S: \RR \sqbrk {\bigcap \mathbb S} = \bigcap_{X \mathop \in \mathbb S} \RR \sqbrk {\mathbb S}$
{{iff}} $\RR$ is a one-to-many relation.
We have that $f$ is a mapping and therefore a many-to-one relation.
So $f$ is a one-to-many relation {{iff}} $f$ is also an injection.
It follows that:
:$\ds \forall \mathbb S \subseteq \powerset S: f \sqbrk {\bigcap \mathbb S} = \bigcap_{X \mathop \in \mathbb S} f \sqbrk X$ 
{{iff}} $f$ is an injection.
{{qed}}
Theorem: Mappings in Product of Sets are Surjections

Let $S$ and $T$ be sets.
Let $\struct {P, \phi_1, \phi_2}$ be a product of $S$ and $T$.
Then $\phi_1$ and $\phi_1$ are surjections.

Proof:
From the definition:
:For all sets $X$ and all mappings $f_1: X \to S$ and $f_2: X \to T$ there exists a unique mapping $h: X \to P$ such that:
::$\phi_1 \circ h = f_1$
::$\phi_2 \circ h = f_2$
Let $X = S$ and let $f_1 = I_S$ where $I_S$ is the identity mapping on $S$.
Then we have:
:$\phi_1 \circ h = I_S$
We have from Identity Mapping is Surjection that $I_S$ is a surjection.
From Surjection if Composite is Surjection it follows that $\phi_1$ is a surjection.
Similarly, let $X = T$ and let $f_2 = I_T$ where $I_T$ is the identity mapping on $T$.
Then we have:
:$\phi_2 \circ h = I_T$
We have from Identity Mapping is Surjection that $I_T$ is a surjection.
From Surjection if Composite is Surjection it follows that $\phi_2$ is a surjection.
{{qed}}
Theorem: Cartesian Product is Set Product

Let $S$ and $T$ be sets.
Let $S \times T$ be the Cartesian product of $S$ and $T$.
Let $\pr_1: S \times T \to S$ and $\pr_2: S \times T \to T$ be the first and second projections respectively on $S \times T$.
Then $\struct {S \times T, \pr_1, \pr_2}$ is a set product.

Proof:
Consider any set $X$ and mappings $f_1: X \to S$ and $f_2: X \to T$.
Define $h: X \to S \times T$ by:
:$\forall x \in X: \map h x = \tuple {\map {f_1} x, \map {f_2} x}$
Then for all $x \in X$ we have:
:$\map {\paren {\pr_1 \mathop \circ h} } x = \pr_1 \tuple {\map {f_1} x, \map {f_2} x} = \map {f_1} x)$
and
:$\map {\paren {\pr_2 \mathop \circ h} } x = \pr_2 \tuple {\map {f_1} x, \map {f_2} x} = \map {f_2} x$
So:
:$\pr_1 \mathop \circ h = f_1$
:$\pr_2 \mathop \circ h = f_2$
Thus $h$ is shown to exist.
Suppose there exists a mapping $k: X \to S \times T$ such that:
:$\pr_1 \mathop \circ k = f_1$
:$\pr_2 \mathop \circ k = f_2$
Let $x \in X$ and let $\map k x = \tuple {s, t}$.
Then:
:$\map {f_1} x = \map {\paren {\pr_1 \mathop \circ k} } x = \map {\pr_1} {s, t} = s$
:$\map {f_2} x = \map {\paren {\pr_2 \mathop \circ k} } x = \map {\pr_2} {s, t} = t$
and so:
{{begin-eqn}}
{{eqn | l = \map k x
      | r = \tuple {s, t}
      | c = 
}}
{{eqn | r = \tuple {\map {f_1} x, \map {f_2} x}
      | c = 
}}
{{eqn | r = \map h x
      | c = 
}}
{{end-eqn}}
and so $k = h$.
So $h$ is unique.
Hence the result.
{{qed}}