avewright/proofwiki-math huggingface dataset:
Theorem: Identity Mapping is Complete Lattice Homomorphism

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

Proof:
=== $\operatorname{id}_A$ is arbitrary join preserving ===
We have:
{{begin-eqn}}
{{eqn | q = \forall X \subseteq A
      | l = \map {\operatorname{id}_A} {\sup X}
      | r = \sup \set{x : x \in X}
}}
{{eqn | r = \sup \set{\map{\operatorname{id}_A} x : x \in X}
}}
{{end-eqn}}
It follows that $\operatorname{id}_A$ is arbitrary join preserving.
{{qed|lemma}}
Theorem: Uniform Prism is Isogonal

Let $P$ be a uniform prism.
Then $P$ is isogonal.

Proof:
{{Recall|Uniform Prism}}
{{:Definition:Uniform Prism}}
Hence $P$ is a regular prism {{afortiori}}.
From Regular Prism is Isogonal, $P$ is isogonal.
Hence the result.
{{qed}}
Category:Uniform Prisms
Category:Isogonal Polyhedra
ki33ojoet4fycuuk5eih4xxctx3doz3
Theorem: Vertical Composition of Natural Transformations is Natural Transformation

Let $\mathbf C$ and $\mathbf D$ be categories.
Let $F, G, H : \mathbf C \to \mathbf D$ be covariant functors.
Let $\eta: F \to G$ and $\xi: G \to H$ be natural transformations.
Then, the vertical composition of $\eta$ and $\xi$:
:$\xi \circ \eta : F \to H$
with
:$\paren {\xi \circ \eta}_X = \xi_X \circ \eta_X$ for each object $X \in C$
is a natural transformation.

Proof:
By definiition of natural transformation and vertical composition:
:For each morphism $f : X \to Y$ in $\mathbf C$, the diagram:
::<nowiki>$\xymatrix{
  F X \ar[d]^{\eta_X} \ar@/_2em/[dd]_{\paren{\xi \circ \eta}_X} \ar[r]^{F f} & F Y \ar[d]^{\eta_Y} \ar@/^2em/[dd]^{\paren{\xi \circ \eta}_Y} \\
  G X \ar[d]^{\xi_X}  \ar[r]^{G f} & F Y \ar[d]^{\xi_Y} \\
  H X \ar[r]^{H f}                 & H Y
}$</nowiki>
:commutes in $\mathbf D$
It follows that for each morphism $f : X \to Y$ in $\mathbf C$:
:{{begin-eqn}}
{{eqn | l = H f \circ \paren{\xi \circ \eta}_X
      | r = \paren{\xi \circ \eta}_Y \circ F f
      | c = 
}}
{{end-eqn}}
Hence the composite of $\eta$ and $\xi$ is a natural transformation by definition.
Theorem: Vertical Composition of Natural Transformations is Natural Transformation

Let $\mathbf C$ and $\mathbf D$ be categories.
Let $F, G, H : \mathbf C \to \mathbf D$ be covariant functors.
Let $\eta: F \to G$ and $\xi: G \to H$ be natural transformations.
Then, the vertical composition of $\eta$ and $\xi$:
:$\xi \circ \eta : F \to H$
with
:$\paren {\xi \circ \eta}_X = \xi_X \circ \eta_X$ for each object $X \in C$
is a natural transformation.

Proof:
For each morphism $f : X \to Y$ in $\mathbf C$, we have:
{{begin-eqn}}
{{eqn | l = H f \circ \paren{\xi \circ \eta}_X
      | r = H f \circ \paren{\xi_X \circ \eta_X}
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{eqn | r = \paren{H f \circ \xi_X} \circ \eta_X
      | c = Associtivity of Composition in $\mathbf D$
}}
{{eqn | r = \paren{\xi_Y \circ G f} \circ \eta_X
      | c = {{Defof|Natural Transformation}} $\xi$
}}
{{eqn | r = \xi_Y \circ \paren{G f  \circ \eta_X}
      | c = Associtivity of Composition in $\mathbf D$
}}
{{eqn | r = \xi_Y \circ \paren{\eta_Y \circ F f}
      | c = {{Defof|Natural Transformation}} $\eta$
}}
{{eqn | r = \paren{\xi_Y \circ \eta_Y} \circ F f
      | c = Associtivity of Composition in $\mathbf D$
}}
{{eqn | r = \paren{\xi \circ \eta}_Y \circ F f
      | c = {{Defof|Vertical Composition of Natural Transformations}}
}}
{{end-eqn}}
Hence the composite of $\eta$ and $\xi$ is a natural transformation by definition.
Theorem: Uniform Antiprism is Isogonal

Let $P$ be a uniform antiprism.
Then $P$ is isogonal.

Proof:
{{Recall|Uniform Antiprism}}
{{:Definition:Uniform Antiprism}}
An equilateral triangle is a special case of an isosceles triangle.
{{Recall|Right-Regular Antiprism}}
{{:Definition:Right-Regular Antiprism}}
Hence $P$ is a right-regular antiprism {{afortiori}}.
From Right-Regular Antiprism is Isogonal, $P$ is isogonal.
Hence the result.
{{qed}}
Category:Uniform Antiprisms
Category:Isogonal Polyhedra
c9q1zausjhrimbc7cedgnayuxah7dju
Theorem: Grothendieck Universe is Closed under Finite Union

Let $\mathbb U$ be a Grothendieck universe.
Let $\set {u_1, u_2, \cdots, u_n : n \in \N} \in \mathbb U$ be a finite subset of elements of $\mathbb U$
Then $\ds \bigcup_{i \mathop \in \N} u_i \in \mathbb U$

Proof:
If $\mathbb U = \O$, the claim is true vacuously.
Assume $\mathbb U \ne \O$.
By Nonempty Grothendieck Universe contains Von Neumann Natural Numbers, $\N \subseteq \mathbb U$.
Grothendieck Universe: Axiom $(4)$ is:
:If $A \in \mathbb U$, and $\set {u_\alpha: \alpha \in A}$ is a family of elements $u_\alpha \in \mathbb U$ indexed by $A$, then $\ds \bigcup_{\alpha \mathop \in A} u_\alpha \in \mathbb U$
Taking $A = \N$, we have:
:$\ds \bigcup_{i \mathop \in \N} u_i \in \mathbb U$
{{qed}}
Category:Grothendieck Universes
n9982vrmlw0y8jb17k53qnnt6ug7cnm
Theorem: Arrow's Impossibility Theorem

Let voters be given $3$ or more distinct choices to choose from.
Then there is no ranking system which can aggregate the individual preferences of two or more individuals so that $4$ apparently reasonable conditions are met.

Proof:
{{ProofWanted}}
{{Namedfor|Kenneth Joseph Arrow|cat = Arrow}}
Theorem: Frame is Distributive Lattice

Let $L= \struct{S, \preceq}$ be a frame.
Then:
:$\struct {S, \vee, \wedge, \preceq}$ is a distributive lattice
where $\vee$ and $\wedge$ denote the join and meet operations on $S$, respectively.

Proof:
By definition of frame:
:$L$ is a complete lattice
From Complete Lattice is Lattice:
:$\struct {S, \vee, \wedge, \preceq}$ is a lattice
By definition of frame:
{{begin-axiom}}
{{axiom | q = \forall a \in S, B \subseteq S
        | m = a \wedge \bigvee B = \bigvee \set {a \wedge b : b \in B}
}}
{{end-axiom}}
Hence:
{{begin-axiom}}
{{axiom | q = \forall a, b_1, b_2 \in S
        | m = a \wedge \paren{b_1 \vee b_2} = \paren{a \wedge b_1} \vee \paren{a \wedge b_2}
}}
{{end-axiom}}
By definition of distributive lattice:
:$\struct {S, \vee, \wedge, \preceq}$ is a distributive lattice
{{qed}}
Category:Frames
Category:Distributive Lattices
00drj6e8a3cv233rmh9whwp7o25bwv6
Theorem: Category CLat is Subcategory of Frm

Let $\mathbf{Frm}$ denote the category of frames.
Let $\mathbf{CLat}$ denote the category of complete lattices.
Then:
:$\mathbf{CLat}$ is a subcategory of $\mathbf{Frm}$

Proof:
From Complete Lattice Homomorphism is Frame Homomorphism:
:$\mathbf{CLat}$ consists of a subcollection of objects and subcollection of morphisms of $\mathbf{Frm}$
By definition of category of complete lattices $\mathbf{CLat}$ and category of frames $\mathbf{Frm}$:
:composition of morphisms in both categories is standard composition of mappings
and:
:identity morphisms in both categories are identity mappings
It follows that $\mathbf{CLat}$ is a subcategory of $\mathbf{Frm}$ by definition.
{{qed}}
Category:Category of Frames (Lattice Theory)
Category:Category of Complete Lattices
4m22e7ev6uwqbu8sevivbzp30s47c9f
Theorem: Adjunction Induces Counit of Adjunction

Let $\mathbf C$, $\mathbf D$ be locally small categories.
Let  $\tuple {F, G, \alpha}$ be an adjunction between $\mathbf C$ and $\mathbf D$.
Let $\beta$ be the inverse of the natural isomorphism $\alpha$.
Then:
:there exists a counit of adjunction $\tuple {F, G, \alpha}$
That is, there exists a natural transformation $\xi: FG \to \operatorname {id}_{\mathbf C}$ where:
:* for each $C$ of $\mathbf C: \xi_{_C} = \map {\beta_{\tuple{GC, C}}} {\operatorname {id}_{GC}}$
:* $\operatorname {id}_{\mathbf C}$ is the identity functor on $\mathbf C$
:* $FG$ is the composite functor of $F$ with $G$

Proof:
From Characterization of Adjunction Using Left Adjuncts of Morphisms, we have:
:$(1):\quad$ for every $g:C_1 \to C_2 \in \mathbf C$:
::$\qquad\qquad\map {\beta_{\tuple{GC_1, C_2} } } {G g} = g \circ \map {\beta_{\tuple{GC_1, C_1} } } {\operatorname{id}_{GC_1}}$
:$(2):\quad$ for every $f:D \to GC \in \mathbf D$:
::$\qquad\qquad\map {\beta_{\tuple{D, C} } } f = \map {\beta_{\tuple{GC, C} } } {\operatorname{id}_{GC} } \circ F f$
For each object $C \in \mathbf C$, let:
:$\xi_{_C} = \map {\beta_{\tuple{GC, C} } } {\operatorname{id}_{GC} }$
Let $m:C_1 \to C_2 \in \mathbf C$ be a morphism.
We have:
{{begin-eqn}}
{{eqn | l = \operatorname{id}_{\mathbf C} m \circ \xi_{C_1}
      | r = m \circ \xi_{C_1}
      | c = {{Defof|Identity Functor}}
}}
{{eqn | r = m \circ \map {\beta_{\tuple{GC_1, C_1} } } {\operatorname{id}_{GC_1} }
      | c = Definition of $\xi_{C_1}$
}}
{{eqn | r = \map {\beta_{\tuple{GC_1, C_2} } } {G m}
      | c = By $(1)$
}}
{{eqn | r = \map {\beta_{\tuple{GC_2, C_2} } } {\operatorname{id}_{GC_2} } \circ FG m 
      | c = By $(2)$
}}
{{eqn | r = \xi_{ {C_2} } \circ FG m
      | c = Definition of $\xi{_{C_2} }$
}}
{{end-eqn}}
It follows that $\xi: FG \to \operatorname {id}_{\mathbf C}$ is a natural transformation.
Hence $\xi$ is the counit of adjunction $\tuple {F, G, \alpha}$ 
{{qed}}
Theorem: Adjunction Induces Unit of Adjunction

Let $\mathbf C$, $\mathbf D$ be locally small categories.
Let  $\tuple {F, G, \alpha}$ be an adjunction between $\mathbf C$ and $\mathbf D$.
Then:
:there exists a unit of adjunction $\tuple {F, G, \alpha}$
That is, there exists a natural transformation $\eta: \operatorname {id}_{\mathbf D} \to GF$ where:
:* for each object $D \in \mathbf D: \eta_{_D} = \map {\alpha_{_\tuple{D, FD}}} {\operatorname {id}_{FD}}$
:* $\operatorname {id}_{\mathbf D}$ is the identity functor on $\mathbf D$
:* $GF$ is the composite functor of $G$ with $F$

Proof:
From Characterization of Adjunction Using Right Adjuncts of Morphisms:
:$\alpha$ associates with:
::objects $D$ in $\mathbf D$ and $C$ in $\mathbf C$
:a bijection:
::$\alpha_{\tuple{D, C} } : \map {\operatorname{Hom}_{\mathbf C} } {FD, C} \to \map {\operatorname{Hom}_{\mathbf D} } {D, GC}$
:such that:
::$(1)\quad$ for every $g:FD \to C \in \mathbf C$:
:::$\qquad\map {\alpha_{\tuple{D, C} } } {g} = Gg \circ \map {\alpha_{\tuple{D, FD} } } {\operatorname{id}_{FD}}$
::$(2)\quad$ for every $f:D_2 \to D_1 \in \mathbf D$:
:::$\qquad\map {\alpha_{\tuple{D_2, FD_1} } } {Ff} = \map {\alpha_{\tuple{D_1, FD_1} } } {\operatorname{id}_{FD_1}} \circ f$
For each object $D \in \mathbf D$, let:
:$\eta_{_D} = \map {\alpha_{\tuple{D, FD}}} {\operatorname {id}_{FD}}$
Let $m: D_1 \to D_2 \in \mathbf D$ be a morphism.
We have:
{{begin-eqn}}
{{eqn | l = \eta_{D_2} \circ \operatorname{id}_{\mathbf D} m
      | r = \eta_{D_2} \circ m
      | c = {{Defof|Identity Functor}}
}}
{{eqn | r = \map {\alpha_{\tuple{D_2, F D_2} } } {\operatorname{id}_{F D_2} } \circ m
      | c = Definition of $\eta_{D_2}$
}}
{{eqn | r = \map {\alpha_{\tuple{D_1, F D_2} } } {F m}
      | c = By $(2)$
}}
{{eqn | r = G F m \circ \map {\alpha_{\tuple{D_1, F D_1} } } {\operatorname{id}_{F D_1} }
      | c = By $(1)$
}}
{{eqn | r = G F m \circ \eta_{ {D_1} }
      | c = Definition of $\eta{_{D_1} }$
}}
{{end-eqn}}
It follows that $\eta: \operatorname {id}_{\mathbf D} \to GF$ is a natural transformation.
Hence $\eta$ is the unit of adjunction $\tuple {F, G, \alpha}$ 
{{qed}}
Theorem: Arzelà's Dominated Convergence Theorem

For each $n \in \N$, let $f_n : \closedint a b \to \R$ be a real function.
Suppose that each $f_n$ is Darboux integrable on $\closedint a b$.
Further suppose that there is a constant $M > 0$ such that:
:$\size {\map {f_n} x} \le M$
for all $n \in \N$ and $x \in \closedint a b$.
Let $\sequence {f_n}$ converge pointwise to a real function $f : \closedint a b \to \R$.
If $f$ is itself Darboux integrable on $\closedint a b$, then:
:$\ds \lim_{n \mathop \to \infty} \int_a^b \size {\map {f_n} x - \map f x} \rd x = 0$
and consequentially:
:$\ds \int_a^b \map f x \rd x = \lim_{n \mathop \to \infty} \int_a^b \map {f_n} x$

Proof:
{{ProofWanted}}
Category:Definite Integrals
g0yet0yfgzomimlfg1r82z1xna0aegm
Theorem: Complex Conjugation is Real Vector Space Automorphism

The operation of complex conjugation:
:$\forall z \in \C: z \mapsto \overline z$
is a vector space automorphism over the real vector space $\R^n$.

Proof:
{{ProofWanted|first define exactly what the above means -- it gets a one-liner in the given source}}
Theorem: Complex Conjugation is not Complex Vector Space Automorphism

The operation of complex conjugation:
:$\forall z \in \C: z \mapsto \overline z$
is ''not'' a vector space automorphism over the complex vector space $\C^n$.

Proof:
{{ProofWanted|first define exactly what the above means -- it gets a one-liner in the given source}}
Theorem: Empty Topological Space is T2

Let $T = \struct {\O, \set \O}$ be the empty topological space.
Then $T$ is a $T_2$ (Hausdorff) space.

Proof:
{{Recall|T2 Space|$T_2$ (Hausdorff) space}}
{{:Definition:T2 Space/Definition 1}}
This is vacuously true for the empty set.
{{qed}}
Category:Empty Topological Space
Category:Examples of Hausdorff Spaces
6jtisofefvxrvtvg7o7n5hczeatzjsx
Theorem: Empty Topological Space is Second Countable

Let $T = \struct {\O, \set \O}$ be the empty topological space.
Then $T$ is second-countable.

Proof:
Follows from Finite Space is Second-Countable.
{{qed}}
Category:Empty Topological Space
9af0xahl6fvkn2jao68vfl5eh1u9uh9
Theorem: Empty Topological Space is Locally Euclidean Space of any Dimension

Let $T = \struct {\O, \set \O}$ be the empty topological space.
Then $T$ is locally euclidean space for every dimension.

Proof:
{{Recall|Locally Euclidean Space}}
{{:Definition:Locally Euclidean Space}}
This is vacuously true for the empty set for every $d \in \N$.
{{qed}}
Category:Empty Topological Space
Category:Locally Euclidean Spaces
h2trl85kjmoc7n9ydfcah3mi5u7xc61
Theorem: Baire Category Theorem/Hausdorff Space

Let $T = \struct {S, \tau}$ be a Hausdorff space.
Let $T$ be locally compact.
Then $T = \struct {S, \tau}$ is also a Baire space.

Proof:
{{ProofWanted}}
{{Namedfor|René-Louis Baire|cat = Baire}}
Theorem: Euclidean Space is Second-Countable

Let $\R^n$ be an $n$-dimensional real vector space.
Let $\struct {\R^n, \tau_d}$ $n$-dimensional real Euclidean space with the usual topology.
Then, $\struct {\R^n, \tau_d}$ is a second-countable space.

Proof:
Let $\struct {\R, \tau}$ be the real line with usual topology.
Let $T_n = \struct {\R^n, \tau_n}$ be the topological space such that $\tau_n$ is the product topology on $\R^n$.
From Real Number Line is Second-Countable, we have that $\struct {\R, \tau}$ is second-countable.
From Countable Product of Second-Countable Spaces is Second-Countable, we have that $\struct {\R^n, \tau_n}$ is second-countable.
From Euclidean Topology is Product Topology, we have that $\tau_d = \tau_n$.
Therefore, $\struct {\R^n, \tau_d}$ is a second-countable space.
{{qed}}
Category:Real Euclidean Spaces
Category:Examples of Second-Countable Spaces
k3rihprvczug4ddy3nqg4u864g8oc3g
Theorem: Empty Topological Space is n-Manifold

Let $T = \struct {\O, \set \O}$ be the empty topological space.
Then $T$ is a topological $n$-manifold for every $n \in \N$.

Proof:
{{Recall|Topological Manifold|topological $d$-manifold}}
{{:Definition:Topological Manifold}}
From Empty Topological Space is $T_2$, $T$ is a $T_2$ space.
From Empty Topological Space is Second Countable, $T$ is second-countable.
From Empty Topological Space is Locally Euclidean Space of any Dimension, $T$ is a locally Euclidean $n$-space for every $n \in \N$.
Therefore, $T$ is a topological $n$-manifold for every $n \in \N$.
{{qed}}
Category:Empty Topological Space
Category:Examples of Topological Manifolds
g0i366a2rvd16vjp4dfo2mcmfqruw67
Theorem: Interior of Topological n-Manifold with Boundary is Topological n-Manifold without Boundary

Let $M$ be a topological $n$-manifold with boundary.
The '''interior''' of $M$, denoted $\Int M$, is a topological $n$-manifold (without boundary).

Proof:
{{Recall|Locally Euclidean Space|locally Euclidean space}}
{{:Definition:Locally Euclidean Space}}
{{Recall|Topological Manifold|manifold (without boundary)}}
{{:Definition:Topological Manifold}}
{{Recall|Topological Manifold with Boundary|manifold with boundary and its interior}}
{{:Definition:Topological Manifold with Boundary}}
{{:Definition:Interior of Topological Manifold with Boundary}}
{{:Definition:Interior Point of Topological Manifold with Boundary}}
{{:Definition:Interior Chart of Topological Manifold with Boundary}}
Hence, $\Int M$ is:
* second-countable,
* Hausdorff, and
* homeomorphic to an open subset of Euclidean space $\R^d$.
Therefore, $\Int M$ is a topological $n$-manifold (without boundary).
{{qed}}
Theorem: Barycentric Coordinates of Centroid of Triangle

Let $\mathbf a$, $\mathbf b$ and $\mathbf c$ be the position vectors of the $3$ vertices of a triangle $T$ in the plane.
Let $p$ be the centroid of $T$.
Let $\alpha$, $\beta$ and $\gamma$ be the barycentric coordinates of $p$ {{WRT}} $T$
Then:
:$\alpha = \beta = \gamma = \dfrac 1 3$

Proof:
thumbalt=A triangle with vertices given by position vectors a, b, and c. The midpoint of bc is marked as q. On the median line aq, the median of the triangle is marked at point p.A [[Definition:Triangletriangle with vertices given by position vectors $\mathbf a$, $\mathbf b$, and $\mathbf c$. The midpoint of $\overline {\mathbf b \mathbf c}$ is marked as $\mathbf q$. On the median line $\overline {\mathbf a \mathbf q}$, the median of the triangle is marked at point $\mathbf p$.]]
Let the position vector $\mathbf q$ be the midpoint of line $\overline {\mathbf b \mathbf c}$.
Parameterize the position of $\mathbf q$ as
:$\mathbf q = \mathbf c + \paren {\mathbf b - \mathbf c} t$
where
:$t \in \mathbb R : 0 < t < 1$
Let the position vector $\mathbf p$ be the median of triangle $T$.
From the definition of the median of a triangle, $\mathbf p$ lies on the line $\overline {\mathbf a \mathbf q}$.
Parameterize the position of $\mathbf p$ as
:$\mathbf p = \mathbf q + \paren {\mathbf a - \mathbf q} s$
where
:$s \in \mathbb R : 0 < s < 1$
Therefore,
{{begin-eqn}}
{{eqn | l = \mathbf p
      | r = \mathbf q + \paren {\mathbf a - \mathbf q} s
}}
{{eqn | r = \mathbf c + \paren {\mathbf b - \mathbf c} t + \paren {\mathbf a - \paren {\mathbf c + \paren {\mathbf b - \mathbf c} t} } s
      | c = Substitute for $\mathbf q$
}}
{{eqn | r = s \mathbf a + \paren {t - s t} \mathbf b + \paren {1 - s - t + s t} \mathbf c
      | c = Simplify
}}
{{end-eqn}}
The barycentric coordinates of $\mathbf p$ are thus
:$\alpha = s$
:$\beta = t - s t$
:$\gamma = 1 - s - t + s t$
These are barycentric coordinates because they satisfy the constraint
:$\alpha + \beta + \gamma = 1$
From the definition of midpoint,
:$t = \dfrac 1 2$
From Position of Centroid of Triangle on Median,
:$s = \dfrac 1 3$
Therefore,
:$\alpha = \dfrac 1 3$
:$\beta = \dfrac 1 2 - \paren {\dfrac 1 3 \cdot \dfrac 1 2} = \dfrac 1 3$
:$\gamma = 1 - \dfrac 1 3 - \dfrac 1 2 + \paren {\dfrac 1 3 \cdot \dfrac 1 2} = \dfrac 1 3$
{{qed}}
Theorem: Ideal and Zero Locus are Order Reversing

Let $k$ be a field.
Let $n \ge 0$ be a natural number.
Let $P := k \sqbrk {x_1, \ldots, x_n}$ be the polynomial ring in $n$ variables over $k$.
Then, the associate ideal and zero-locus are inclusion reversing.
That is:
:$(1): \quad$ if:
::::$X \subseteq Y \subseteq k^n$
:::then:
::::$\map I Y \subseteq \map I X$
:$(2): \quad$ if:
::::$I \subseteq J \subseteq k \sqbrk {x_1, \ldots, x_n}$ are ideals of $k \sqbrk {x_1, \ldots, x_n}$
:::then:
::::$\map Z J \subseteq \map Z I$

Proof:
;<nowiki>$(1):$</nowiki> zero-locus is inclusion reversing
By definition, the '''zero locus''' of $I$ is the set:
:$\map V I = \set {x \in k^n : \forall f \in I: \map f x = 0}$
Let $X \subseteq Y \subseteq k^n$ be nested sets. 
Let $p \in k \sqbrk {x_1, \ldots, x_n}$ be a polynomial in $k$ such that $p$ vanishes on $Y$.
As $X \subseteq Y$, it follows that $p$ vanishes on $X$.
Hence:
:$\map I Y \subseteq \map I X$
{{qed|lemma}}
{{Explain|I'm not sure I've got this right. Which is the zero locus and which is the ideal? It looks like it would make more sense to denote $\map I Y$ as the ideal and $\map Z Y$ as the zero locus. As it is, unless I misunderstand, which is almost surely the case, then the first part demonstrates the zero locus being inclusion reversing and the second part demonstrates the associate ideal being inclusion reversing. IN any case, further elaboration of exactly what is being done here would make this proof comprehensible to the casual reader who may not be completely familiar with all the details of the elements of this area of mathematics.}}
;<nowiki>$(2):$</nowiki> associate ideal  is inclusion reversing
Let $I \subseteq J \subseteq k \sqbrk {x_1, \ldots, x_n}$ be ideals of $k \sqbrk {x_1, \ldots, x_n}$.
Let $x \in k^n$ is a vanishing point of $J$.
Then $\map p x = 0$ for all $p \in J$.
As $I \subseteq J$, it follows that $\map p x = 0$ for all $p \in I$.
Hence:
:$\map Z J \subseteq \map Z I$
Hence the result.
{{qed}}
Category:Algebraic Geometry
7rn3ppnhb1fhx2zbpn0bzkv7b5hwadt
Theorem: Bellman's Principle of Optimality

Let $P$ be an optimal path in an exercise in dynamic programming.
Then any part of $P$ is also an optimal path.

Proof:
{{ProofWanted}}
{{Namedfor|Richard Ernest Bellman|cat = Bellman}}
Theorem: Benford's Law

'''Benford's law''' is an empirical observation concerning the leading digits in a given number base (usually $10$).
In a data set containing data spanning several orders of magnitude, the leading digits are more likely to be small.

Proof:
{{ProofWanted}}
{{Namedfor|Frank Albert Benford|cat = Benford}}
Theorem: Direct Image Mapping of Identity is Identity

Let $S$ be a set.
Let $I_S : S \to S$ be the identity mapping on $S$.
Let $\paren{I_S}^\to : \powerset S \to \powerset S$ be the direct image mapping of $I_S$.
Then:
:$\paren{I_S}^\to = I_{\powerset S}$
where $I_{\powerset S} :\powerset S \to \powerset S$ denotes the identity mapping on $\powerset S$.

Proof:
Let $A \in \powerset S$.
We have:
{{begin-eqn}}
{{eqn | q = \forall A \in \powerset S
      | l = \map {\paren{I_S}^\to} A
      | r = \set{x \in S : \exists y \in A : \map {I_S} y = x}
      | c = {{Defof|Direct Image Mapping}}
}}
{{eqn | ll = \leadsto
      | q = \forall A \in \powerset S
      | l = A
      | o = \subseteq
      | r = \map {\paren{I_S}^\to} A
      | c = {{Defof|Identity Mapping}}
}}
{{eqn | ll = \leadsto
      | q = \forall A \in \powerset S
      | l = S \setminus A
      | o = \subseteq
      | r = S \setminus \map {\paren{I_S}^\to} A
      | c = {{Defof|Identity Mapping}}
}}
{{eqn | ll = \leadsto
      | q = \forall A \in \powerset S
      | l = \map {\paren{I_S}^\to} A
      | o = \subseteq
      | r = A
      | c = Relative Complement inverts Subsets
}}
{{eqn | ll = \leadsto
      | q = \forall A \in \powerset S
      | l = \map {\paren{I_S}^\to} A
      | r = A
      | c = {{Defof|Set Equality}}
}}
{{eqn | ll = \leadsto
      | q = \forall A \in \powerset S
      | l = \map {\paren{I_S}^\to} A
      | r = \map {I_{\powerset S} } A
      | c = {{Defof|Identity Mapping}}
}}
{{eqn | ll = \leadsto
      | l = \paren{I_S}^\to
      | r = I_{\powerset S} 
      | c = Equality of Mappings
}}
{{end-eqn}}
{{qed}}
Category:Direct Image Mappings
Category:Inverse Mappings
ohjxk6f0cub5qr5gaim1bvgr5t63xtv
Theorem: Inverse of Direct Image Mapping is Direct Image Mapping of Inverse

Let $S$ and $T$ be sets.
Let $f :S \to T$ be a bijection.
Let $f^\to$ be the direct image mapping of $f$.
Then:
:$\paren {f^\to}^{-1} = \paren {f^{-1} }^{\to}$
where $f^{-1}$ and $\paren{f^\to}^{-1}$ denote the inverses of $f$ and $f^\to$ respectively

Proof:
From Mapping is Bijection iff Direct Image Mapping is Bijection:
:$f^\to$ is a bijection
From Bijection has Left and Right Inverse:
:the inverses $f^{-1}$ and $\paren{f^\to}^{-1}$ are well-defined
We have:
{{begin-eqn}}
{{eqn | l = f^\to \circ \paren{f^{-1} }^\to
      | r = \paren{f \circ f^{-1} }^\to
      | c = Composition of Direct Image Mappings of Mappings
}}
{{eqn | r = \paren{I_S }^\to
      | c = {{Defof|Inverse Mapping}}
}}
{{eqn | r = I_{\powerset S}
      | c = Direct Image Mapping of Identity is Identity
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = \paren{f^{-1} }^\to \circ f^\to 
      | r = I_{\powerset T}
}}
{{end-eqn}}
Hence $\paren {f^\to}^{-1} = \paren {f^{-1} }^{\to}$ by definition of inverse mapping.
{{qed}}
Category:Direct Image Mappings
Category:Identity Mappings
h9fxohuonwct968v1emufuzfxhiwerk