avewright/proofwiki-math huggingface dataset:
Theorem: Mediant is Dependent upon Representation

Let $r, s \in \Q$ be rational numbers.
Let $r$ and $s$ be expressed as:
{{begin-eqn}}
{{eqn | l = r
      | r = \dfrac a b
}}
{{eqn | l = s
      | r = \dfrac c d
}}
{{end-eqn}}
where $a, b, c, d$ are integers such that $b > 0, d > 0$.
Then the mediant of $r$ and $s$ is dependent upon the specific integers chosen for $a, b, c, d$.

Proof:
;Proof by Counterexample
Let $r = \dfrac 1 2$ and $s = 1$.
We have:
:$r = \dfrac 1 2 = \dfrac 2 4 = \dfrac 3 6$
Then the mediant of $r = \dfrac 2 4$ and $s = \dfrac 1 1$ gives: 
:$\dfrac {2 + 1} {4 + 1} = \dfrac 3 5$
but the mediant of $r = \dfrac 1 2$ and $s = \dfrac 1 1$ gives: 
:$\dfrac {1 + 1} {2 + 1} = \dfrac 2 3$
which is not the same as $\dfrac {2 + 1} {4 + 1}$.
{{qed}}
Theorem: All Infima Preserving Mapping is Upper Adjoint of Galois Connection/Lemma 1

:$g$ is an increasing mapping.

Proof:
Define a mapping $d: T \to S$:
:$\forall t \in T: \map d t := \map \inf {g^{-1} \sqbrk {t^\succsim} }$
Let $x, y \in S$ such that
:$x \preceq y$
By Upper Closure is Decreasing:
:$y^\succeq \subseteq x^\succeq$
By Infimum of Upper Closure of Element:
:$\map \inf {x^\succeq} = x$ and $\map \inf {y^\succeq} = y$
By definition of all infima preserving mapping:
:$g$ preserves the infimum on $x^\succeq$
and:
:$g$ preserves the infimum on $y^\succeq$
By definition of infimum on subset preserving mapping:
:$\map \inf {\map {g^\to} {x^\succeq} } = \map g x$ and $\map \inf {\map {g^\to} {y^\succeq} } = \map g y$
By Image of Subset under Mapping is Subset of Image:
:$\map {g^\to} {y^\succeq} \subseteq \map {g^\to} {x^\succeq}$
Thus by Infimum of Subset:
:$\map g x \precsim \map g y$
{{qed}}
Theorem: Category Axioms are Self-Dual/Object Category Theory

Let $\mathrm {CT}$ be the collection of seven axioms on Characterization of Metacategory via Equations.
Then:
:$\mathrm {CT} = \mathrm {CT}^*$
where $\mathrm {CT}^*$ consists of the dual statements of those in $\mathrm{CT}$.

Proof:
The seven axioms are:
{{begin-eqn}}
{{eqn | l = \operatorname {dom} \operatorname {id}_A = A
      | o = \qquad
      | r = \operatorname {cod} \operatorname {id}_A = A
}}
{{eqn | l = f \circ 1_{\operatorname {dom} f} = f
      | o = 
      | r = 1_{\operatorname {cod} f} \circ f = f
}}
{{eqn | l = \map {\operatorname {dom} } {g \circ f} = \operatorname{dom} f
      | o = 
      | r = \map {\operatorname {cod} } {g \circ f} = \operatorname{cod} g
}}
{{eqn | l = h \circ \paren {g \circ f}
      | r = \paren {h \circ g} \circ f
}}
{{end-eqn}}
Their duals are:
{{begin-eqn}}
{{eqn | l = \operatorname {cod} \operatorname {id}_A = A
      | o = \qquad
      | r = \operatorname {dom} \operatorname {id}_A = A
}}
{{eqn | l = 1_{\operatorname {cod} f} \circ f = f
      | o = 
      | r = f \circ 1_{\operatorname {dom} f} = f
}}
{{eqn | l = \map {\operatorname {cod} } {f \circ g} = \operatorname {cod} f
      | o = 
      | r = \map {\operatorname {dom} } {f \circ g} = \operatorname {dom} g
}}
{{eqn | l = \paren {f \circ g} \circ h
      | r = f \circ \paren {g \circ h}
}}
{{end-eqn}}
It is seen that only names of the bound variables $f, g$ and $h$ have been changed at some places.
Therefore, we conclude:
:$\mathrm {CT}^* = \mathrm {CT}$
{{qed}}
Theorem: Distribution Space over Smooth Functions is Unitary Module

The distribution space over smooth functions is a unitary module.

Proof:
Let $\phi \in \map \DD {\R^d}$ be a test function.
Theorem: Smooth Real Function times Derivative of Dirac Delta Distribution/Corollary

Let $\delta \in \map {\DD'} \R$ be the Dirac delta distribution.
Then in the distributional sense it holds that:
:$x \delta' = -\delta$

Proof:
From Smooth Real Function times Derivative of Dirac Delta Distribution:
:$\alpha \cdot \delta' = \map \alpha 0 \delta' - \map {\alpha'} 0 \delta$
where $\alpha$ is a smooth function.
If $\map \alpha x = x$, then:
:$x \delta' = -\delta$
{{qed}}
Theorem: Hamiltonian Graph is not necessarily Ore Graph

Let $G = \struct {V, E}$ be a simple graph of order $n \ge 3$.
Let $G$ be a Hamiltonian graph.
Then $G$ is not necessarily an Ore graph.

Proof:
Proof by Counterexample:
Recall the definition of an Ore graph:
:For each pair of non-adjacent vertices $u, v \in V$:
::$\deg u + \deg v \ge n$
Let $n \in \N$ such that $n \ge 5$.
Consider the cycle graph $C_n$.
We have from Cycle Graph is Hamiltonian that $C_n$ is a Hamiltonian graph.
We also have from Cycle Graph is 2-Regular that all the vertices of $C_n$ are of degree $2$.
Let $u, v \in C_n$ such that $u$ and $v$ are non-adjacent.
Such a pair is always possible to find in $C_n$.
Then:
:$\deg u + \deg v  = 4 < n$
so $C_n$ is not an Ore graph.
{{qed}}
Theorem: Sum of Integrals on Adjacent Intervals for Integrable Functions/Lemma

Let $\closedint a b$ be a closed real interval.
Let $c$ be a real number.
Let $a < c < b$.
Let $f$ be a real function defined on $\closedint a b$.
Let $\map L S$ be the lower Darboux sum of $f$ on $\closedint a b$ where $S$ is a subdivision of $\closedint a b$.
Let $P$ and $Q$ be finite subdivisions of $\closedint a b$.
Let:
:$Q = P \cup \set c$.
Then:
:$\map L Q \ge \map L P$

Proof:
This is an instance of Lower Sum of Refinement.
{{qed}}
Theorem: Sum of Integrals on Adjacent Intervals for Integrable Functions/Lemma

Let $\closedint a b$ be a closed real interval.
Let $c$ be a real number.
Let $a < c < b$.
Let $f$ be a real function defined on $\closedint a b$.
Let $\map L S$ be the lower Darboux sum of $f$ on $\closedint a b$ where $S$ is a subdivision of $\closedint a b$.
Let $P$ and $Q$ be finite subdivisions of $\closedint a b$.
Let:
:$Q = P \cup \set c$.
Then:
:$\map L Q \ge \map L P$

Proof:
Let $P = \set {x_0, x_1, \ldots, x_n}$.
Suppose that:
:$c \in P$
Then:
:$Q = P$
We have:
:$\map L P \ge \map L P$
:$\leadsto \map L Q \ge \map L P$ as $Q = P$
This finishes the proof for this case.
The only other possibility for $c$ is:
:$x_{j-1} < c < x_j$
where $1 \le j \le n$.
Let $m_i$ be the infimum of $f$ on the interval $\closedint {x_{i - 1}} {x_i}$ for all $i \in \set {1, 2, \ldots, n}$.
We have:
{{begin-eqn}}
{{eqn | l = \map L P
      | r = \sum_{i \mathop = 1}^n m_i \paren {x_i - x_{i - 1} }
      | c = {{Defof|Lower Darboux Sum}}
}}
{{eqn | r = \sum_{i \mathop = 1}^{j - 1} m_i \paren {x_i - x_{i - 1} } + m_j \paren {x_j - x_{j - 1} }  + \sum_{i \mathop = j + 1}^n m_i \paren {x_i - x_{i - 1} }
}}
{{eqn | r = \sum_{i \mathop = 1}^{j - 1} m_i \paren {x_i - x_{i - 1} } + m_j \paren {x_j − c + c - x_{j - 1} } + \sum_{i \mathop = j + 1}^n m_i \paren {x_i - x_{i - 1} }
}}
{{eqn | r = \sum_{i \mathop = 1}^{j - 1} m_i \paren {x_i - x_{i - 1} } + m_j \paren {x_j − c} + m_j \paren {c - x_{j - 1} } + \sum_{i \mathop = j + 1}^n m_i \paren {x_i - x_{i - 1} }
}}
{{eqn | r = \sum_{i \mathop = 1}^{j - 1} m_i \paren {x_i - x_{i - 1} } + m_j \paren {c - x_{j - 1} } + m_j \paren {x_j − c} + \sum_{i \mathop = j + 1}^n m_i \paren {x_i - x_{i - 1} }
}}
{{end-eqn}}
Let $r$ be the infimum of $f$ on the interval $\closedint {x_{j - 1}} c$.
Let $s$ be the infimum of $f$ on the interval $\closedint c {x_j}$.
The interval $\closedint {x_{j - 1}} c$ is a subset of $\closedint {x_{j - 1}} {x_j}$.
Therefore, a lower bound of $f$ on the interval $\closedint {x_{j - 1}} {x_j}$ is a lower bound of $f$ on the interval $\closedint {x_{j - 1}} c$ as well.
The infimum of $f$ on the interval $\closedint {x_{j - 1}} {x_j}$ is a lower bound for $f$ on this interval.
Accordingly, the infimum of $f$ on the interval $\closedint {x_{j - 1}} {x_j}$ is a lower bound of $f$ on the interval $\closedint {x_{j - 1}} c$ as well.
Therefore, the infimum of $f$ on the interval $\closedint {x_{j - 1}} c$ is greater than or equal to the infimum of $f$ on the interval $\closedint {x_{j - 1}} {x_j}$.
In other words:
:$r \ge m_j$
A similar analysis of $\closedint c {x_j}$ gives:
:$s \ge m_j$
We find:
{{begin-eqn}}
{{eqn | l = \map L P
      | r = \sum_{i \mathop = 1}^{j - 1} m_i \paren {x_i - x_{i - 1} } + m_j \paren {c - x_{j - 1} } + m_j \paren {x_j − c} + \sum_{i \mathop = j + 1}^n m_i \paren {x_i - x_{i - 1} }
}}
{{eqn | o = \le
      | r = \sum_{i \mathop = 1}^{j - 1} m_i \paren {x_i - x_{i - 1} } + r \paren {c - x_{j - 1} } + s \paren {x_j − c} + \sum_{i \mathop = j + 1}^n m_i \paren {x_i - x_{i - 1} }
}}
{{eqn | r = \map L Q
      | c = {{Defof|Lower Darboux Sum}}
}}
{{end-eqn}}
This finishes the proof.
{{qed}}
Theorem: Intersection of Class and Set is Set

Let $C$ be the class:
:$C = \set { u : \map \phi {u, p_1, \ldots, p_n} }$
Then for all sets $X$, $C \cap X$ is a set.

Proof:
{{NotZFC}}
By the definition of class intersection:
:$a \in C \cap X \implies a \in C \land a \in X$
Thus:
:$a \in C \cap X \implies a \in X$
The subclass definition gives:
:$C \cap X \subseteq X$
By Subclass of Set is Set, $C \cap X$ is a set.
{{qed}}
Theorem: If Set Exists then Empty Set Exists

If at least one set exists, then there exists an empty set.

Proof:
{{NotZFC}}
Let $S$ be a set.
By the axiom of class comprehension, there is an empty class:
:$\O = \set { x : x \ne x }$
Since $x \in \O$ is never true, it follows vacuously that:
:$x \in \O \implies x \in S$
By the subclass definition:
:$\O \subseteq S$
By Subclass of Set is Set, $\O$ is a set.
{{qed}}
Theorem: Powerset is not Subset of its Set

Let $A$ be a set.
Then:
:$\powerset A \not \subseteq A$

Proof:
{{AimForCont}} that $\powerset A \subseteq A$, and define:
:$C = \set {x \in \powerset A : x \notin x}$
We have that $C \subseteq \powerset A$, as it contains only the $x \in \powerset A$ meeting the condition $x \notin x$.
Since $\powerset A \subseteq A$, we have:
:$C \subseteq A$
and thus
:$C \in \powerset A$
We can derive a similar contradiction to Russell's Paradox.
If $C \in C$, then it must meet $C$'s condition that $C \notin C$.
If $C \notin C$, then it meets $C$'s condition for $C \in C$.
{{qed}}
Theorem: Powerset is not Subset of its Set

Let $A$ be a set.
Then:
:$\powerset A \not \subseteq A$

Proof:
{{AimForCont}} that $\powerset A \subseteq A$.
Let $I: \powerset A \to A$ be the identity mapping.
$I$ is an injection by Identity Mapping is Injection.
But by No Injection from Power Set to Set, this is a contradiction.
{{qed}}
Theorem: Powerset is not Subset of its Set

Let $A$ be a set.
Then:
:$\powerset A \not \subseteq A$

Proof:
{{AimForCont}} that $\powerset A \subseteq A$.
Since $A \in \powerset A$, this implies:
:$A \in A$
But this contradicts Set is Not Element of Itself.
{{qed}}
Theorem: Integer which is Multiplied by Last Digit when moving Last Digit to First

Let $N$ be a positive integer expressed in decimal notation in the form:
:$N = \sqbrk {a_k a_{k - 1} a_{k - 2} \ldots a_2 a_1}_{10}$
Let $N$ be such that when you multiply it by $a_1$, you get:
:$a_1 N = \sqbrk {a_1 a_k a_{k - 1} \ldots a_3 a_2}_{10}$
Then at least one such $N$ is equal to the recurring part of the fraction:
:$q = \dfrac {a_1} {10 a_1 - 1}$

Proof:
Let us consider:
:$q = 0 \cdotp \dot a_k a_{k - 1} a_{k - 2} \ldots a_2 \dot a_1$
Let:
:$a_1 q = 0 \cdotp \dot a_1 a_k a_{k - 1} \ldots a_3 \dot a_2$
Then:
{{begin-eqn}}
{{eqn | l = 10 a_1 q
      | r = a_1 \cdotp \dot a_k a_{k - 1} a_{k - 2} \ldots a_2 \dot a_1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 10 a_1 q - a_1
      | r = 0 \cdotp \dot a_k a_{k - 1} a_{k - 2} \ldots a_2 \dot a_1
      | c = 
}}
{{eqn | r = q
      | c = 
}}
{{eqn | ll= \leadsto
      | l = q
      | r = \dfrac {a_1} {10 a_1 - 1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Recreational Mathematics
o4pp86gjsc3tflfqiln725jndwpk5k0
Theorem: Weak Solution to Dx u + 3yu = 0 with Heaviside Step Function Boundary Condition

Consider the boundary value problem:
:<nowiki>$\begin{cases}
\dfrac {\partial u} {\partial x} + 3 y u = 0 & : x \in \R_{>0},~ y \in \R \\
& \\
\map u {0, y} = \map H y & : y \in \R \\
\end{cases}$</nowiki>
Then it has a weak solution of the form:
:$u = e^{-3 y x} \map H y$

Proof:
Let $u = e^{-3 y x} \map H y$
We have that:
:Heaviside Step Function is Locally Integrable
:Locally Integrable Function defines Distribution
:Multiplication of Distribution induced by Locally Integrable Function by Smooth Function
Hence, we can define a distribution $T_u \in \map {\DD'} {\R^2}$ associated with $u$.
Then in the distributional sense we have that:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial u} {\partial x}
      | r = \dfrac \partial {\partial x} \paren {e^{-3 y x} \map H y}
}}
{{eqn | r = e^{-3 y x} \paren {-3 y} \map H y + e^{-3 y x} \dfrac {\partial \map H y} {\partial x}
}}
{{end-eqn}}
That is:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial T_u} {\partial x}
      | r = \dfrac \partial {\partial x} T_{e^{-3 y x} \map H y}
}}
{{eqn | r = \dfrac \partial {\partial x} \paren {e^{-3 y x} T_{\map H y} }
      | c = Multiplication of Distribution induced by Locally Integrable Function by Smooth Function
}}
{{eqn | r = e^{-3 y x} \paren {-3 y} T_{\map H y} + e^{-3 y x} \dfrac \partial {\partial x} T_{\map H y}
      | c = Product Rule for Distributional Derivatives of Distributions multiplied by Smooth Functions
}}
{{end-eqn}}
Let $\phi \in \map \DD {\R^2}$ be a test function.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial}{\partial x} \map {T_{\map H y} } \phi
      | r = - \map {T_{\map H y} } {\dfrac {\partial \phi}{\partial x} }
}}
{{eqn | r = - \int_{-\infty}^\infty \int_{-\infty}^\infty \map H y \dfrac {\partial \phi}{\partial x} \rd x \rd y
}}
{{eqn | r =  - \int_0^\infty \int_{-\infty}^\infty \dfrac {\partial \phi}{\partial x} \rd x \rd y
}}
{{eqn | r = - \int_0^\infty \paren {\bigintlimits {\map \phi {x, y} } {x \mathop = - \infty} {x \mathop = \infty} } \rd y
}}
{{eqn | r = - \int_0^\infty 0 \rd y
      | c = {{Defof|Test Function}}
}}
{{eqn | r = 0
}}
{{end-eqn}}
Hence, in the distributional sense we have that:
:$\dfrac \partial {\partial x} \map H y = \mathbf 0$
where $\mathbf 0$ is the zero distribution.
Therefore:
{{begin-eqn}}
{{eqn | l = \dfrac {\partial u} {\partial x} + 3 y u
      | r = e^{-3xy} \paren {-3y} \map H y + 3y e^{-3yx} \map H y
}}
{{eqn | r = \mathbf 0
}}
{{end-eqn}}
Moreover:
{{begin-eqn}}
{{eqn | l = \map u {0, y}
      | r = e^{-0} \map H y
}}
{{eqn | r = \map H y
}}
{{end-eqn}}
{{qed}}
Theorem: Divisors of One More than Power of 10/Number of Zero Digits Congruent to 2 Modulo 3

Let $N$ be a natural number of the form:
:$N = 1000 \ldots 01$
where the number of zero digits between the two $1$ digits is of the form $3 k - 1$.
Then $N$ has divisors:
::$1 \underbrace {00 \ldots 0}_{\text {$k - 1$ $0$'s} } 1$
:where the number of zero digits between the two $1$ digits is $k - 1$
::$\underbrace {99 \ldots 9}_{\text {$k$ $9$'s} } \underbrace {00 \ldots 0}_{\text {$k - 1$ $0$'s} }1$

Proof:
By definition, $N$ can be expressed as:
:$N = 10^{3 k} + 1$
Let $a := 10^k$.
Then we have:
{{begin-eqn}}
{{eqn | l = N
      | r = a^3 + 1
      | c = 
}}
{{eqn | r = \paren {a + 1} \paren {a^2 - a + 1}
      | c = Sum of Two Cubes
}}
{{end-eqn}}
where it is noted that:
{{begin-eqn}}
{{eqn | l = \underbrace {99 \ldots 9}_{\text {$k$ $9$'s} } \underbrace {00 \ldots 0}_{\text {$k - 1$ $0$'s} }1
      | r = \underbrace {99 \ldots 9}_{\text {$k$ $9$'s} } \underbrace {00 \ldots 0}_{\text {$k$ $0$'s} } + 1
      | c = 
}}
{{eqn | r = 10^k \paren {\underbrace {99 \ldots 9}_{\text {$k$ $9$'s} } } + 1
      | c = 
}}
{{eqn | r = 10^k \paren {10^k - 1} + 1
      | c = 
}}
{{eqn | r = a^2 - a + 1
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Divisors of One More than Power of 10/Number of Zero Digits Even

Let $N$ be a natural number of the form:
:$N = 1 \underbrace {000 \ldots 0}_{\text {$2 k$ $0$'s} } 1$
that is, where the number of zero digits between the two $1$ digits is even.
Then $N$ can be expressed as:
:$N = 11 \times \underbrace {9090 \ldots 90}_{\text {$k - 1$ $90$'s} } 91$

Proof:
By definition, $N$ can be expressed as:
:$N = 10^{2 k + 1} + 1$
Then we have:
{{begin-eqn}}
{{eqn | l = N
      | r = 10^{2 k + 1} + 1
      | c = 
}}
{{eqn | r = \paren {10 + 1} \sum_{j \mathop = 0}^{2 k} \paren {-1}^j 10^{2 k - j}
      | c = Sum of Two Odd Powers
}}
{{eqn | ll= \leadsto
      | l = \dfrac N {11} 
      | r = \sum_{j \mathop = 0}^{2 k} \paren {-1}^j 10^{2 k - j}
      | c = 
}}
{{eqn | r = 10^{2 k} - 10^{2 k - 1} + 10^{2 k - 2} - 10^{2 k - 3} + \cdots + 10^2 - 10^1 + 10^0
      | c = 
}}
{{eqn | r = 10^{2 k - 1} \paren {10 - 1} + 10^{2 k - 3} \paren {10 - 1} + \cdots + 10 \paren {10 - 1} + 1
      | c = 
}}
{{eqn | r = 90 \paren {10^{2 k - 2} + 10^{2 k - 4} + \cdots + 10^0} + 1
      | c = 
}}
{{eqn | r = 90 \sum_{j \mathop = 0}^k \paren {10^{2 j} } + 1
      | c = 
}}
{{eqn | r = \underbrace {9090 \ldots 90}_{\text {$k$ $90$'s} } + 1
      | c = 
}}
{{eqn | r = \underbrace {9090 \ldots 90}_{\text {$k - 1$ $90$'s} } 91
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Complement of Horizontal Section of Set is Horizontal Section of Complement

Let $X$ and $Y$ be sets.
Let $E \subseteq X \times Y$. 
Let $y \in Y$. 
Then: 
:$\paren {\paren {X \times Y} \setminus E}^y = X \setminus E^y$
where:
:$\paren {\paren {X \times Y} \setminus E}^y$ is the $y$-horizontal section of the set difference $\paren {X \times Y} \setminus E$
:$E^y$ is the $y$-horizontal section of $E$.

Proof:
Note that from the definition of set difference, we have that: 
:$x \in X \setminus E^y$
{{iff}}: 
:$x \in X$ and $x \not \in E^y$.
That is, from the definition of the $y$-horizontal section: 
:$x \in X$ and $\tuple {x, y} \not \in E$.
This is equivalent to: 
:$\tuple {x, y} \in \paren {X \times Y} \setminus E$
From the definition of the $y$-horizontal section, this is then equivalent to: 
:$x \in \paren {\paren {X \times Y} \setminus E}^y$
So we have:
:$x \in X \setminus E^y$ {{iff}} $x \in \paren {\paren {X \times Y} \setminus E}^y$.
So:
:$\paren {\paren {X \times Y} \setminus E}^y = X \setminus E^y$
{{qed}}
Category:Horizontal Section of Sets
gui6cwpqbp02kpmr5th0gd89gvtdw3m
Theorem: Complement of Vertical Section of Set is Vertical Section of Complement

Let $X$ and $Y$ be sets.
Let $E \subseteq X \times Y$. 
Let $x \in X$. 
Then: 
:$\paren {\paren {X \times Y} \setminus E}_x = Y \setminus E_x$
where:
:$\paren {\paren {X \times Y} \setminus E}_x$ is the $x$-vertical section of the set difference $\paren {X \times Y} \setminus E$
:$E_x$ is the $x$-vertical section of $E$.

Proof:
Note that from the definition of set difference, we have that: 
:$y \in Y \setminus E_x$
{{iff}}: 
:$y \in Y$ and $y \not \in E_x$.
That is, from the definition of the $x$-vertical section: 
:$y \in Y$ and $\tuple {x, y} \not \in E$.
This is equivalent to:
:$\tuple {x, y} \in \paren {X \times Y} \setminus E$ 
From the definition of the $x$-vertical section, this is then equivalent to: 
:$y \in \paren {\paren {X \times Y} \setminus E}_x$
So we have:
:$y \in Y \setminus E_x$ {{iff}} $y \in \paren {\paren {X \times Y} \setminus E}_x$.
So:
:$\paren {\paren {X \times Y} \setminus E}_x = Y \setminus E_x$
{{qed}}
Category:Vertical Section of Sets
pagbln3czuj1g2z525hz9qc97yuoiu9
Theorem: Union of Horizontal Sections is Horizontal Section of Union

Let $X$, $Y$ and $A$ be sets.
Let $\set {E_\alpha : \alpha \in A}$ be a set of subsets of $X \times Y$. 
Let $y \in Y$. 
Then: 
:$\ds \paren {\bigcup_{\alpha \mathop \in A} E_\alpha}^y = \bigcup_{\alpha \mathop \in A} \paren {E_\alpha}^y$
where:
:$\ds \paren {\bigcup_{\alpha \mathop \in A} E_\alpha}^y$ is the $y$-horizontal section of $\ds \bigcup_{\alpha \mathop \in A} E_\alpha$
:$\paren {E_\alpha}^y$ is the $y$-horizontal section of $E_\alpha$.

Proof:
Note that:
:$\ds x \in \bigcup_{\alpha \mathop \in A} \paren {E_\alpha}^y$
{{iff}}: 
:$x \in \paren {E_\alpha}^y$ for some $\alpha \in A$.
From the definition of the $y$-horizontal section, this is equivalent to:
:$\tuple {x, y} \in E_\alpha$ for some $\alpha \in A$. 
This in turn is equivalent to: 
:$\ds \tuple {x, y} \in \bigcup_{\alpha \mathop \in A} E_\alpha$
Again applying the definition of the $y$-horizontal section, this is the case {{iff}}:
:$\ds x \in \paren {\bigcup_{\alpha \mathop \in A} E_\alpha}^y$
So:
:$\ds x \in \bigcup_{\alpha \mathop \in A} \paren {E_\alpha}^y$ {{iff}} $\ds x \in \paren {\bigcup_{\alpha \mathop \in A} E_\alpha}^y$
giving:
:$\ds \paren {\bigcup_{\alpha \mathop \in A} E_\alpha}^y = \bigcup_{\alpha \mathop \in A} \paren {E_\alpha}^y$
{{qed}}
Category:Set Union
Category:Horizontal Section of Sets
515hfga7amdk2466rutfb9mozglopen
Theorem: Horizontal Section of Cartesian Product

Let $X$ and $Y$ be sets.
Let $A \subseteq X$ and $B \subseteq Y$, so that $A \times B \subseteq X \times Y$. 
Let $y \in Y$. 
Then: 
:$\paren {A \times B}^y = \begin{cases}A & y \in B \\ \O & y \not \in B\end{cases}$
where $\paren {A \times B}^y$ is a horizontal section of $A \times B$.

Proof:
Let $y \in B$. 
From the definition of the horizontal section, we have: 
:$x \in \paren {A \times B}^y$
{{iff}}:
:$\tuple {x, y} \in A \times B$ 
Since $y \in B$, this equivalent to: 
:$x \in A$
So:
:$x \in \paren {A \times B}^y$ {{iff}} $x \in A$
giving:
:$\paren {A \times B}^y = A$ if $y \in B$.
Now let $y \in Y \setminus B$.
So, by the definition of set difference, we have $y \in Y$ and $y \not \in B$.
As before, we have:
:$x \in \paren {A \times B}^y$ 
{{iff}}:
:$\tuple {x, y} \in A \times B$
But this is equivalent to: 
:$x \in A$ and $y \in B$.
Since $y \not \in B$, there exists no $x \in \paren {A \times B}^y$.
So:
:$\paren {A \times B}^y = \O$ if $y \not \in B$.
{{qed}}
Category:Horizontal Section of Sets
Category:Cartesian Product
ms3edjkpygg4ilo2hqgs4erzu6m8m1w
Theorem: Horizontal Section of Measurable Set is Measurable

Let $\struct {X, \Sigma_X}$ and $\struct {Y, \Sigma_Y}$ be measurable spaces. 
Let $E \in \Sigma_X \otimes \Sigma_Y$ where $\Sigma_X \otimes \Sigma_Y$ is the product $\sigma$-algebra of $\Sigma_X$ and $\Sigma_Y$.
Let $y \in Y$. 
Then: 
:$E^y \in \Sigma_X$
where $E^y$ is the $y$-horizontal section of $E$.

Proof:
Define $f_y : X \to X \times Y$ by: 
:$\map {f_y} x = \tuple {x, y}$ 
for each $x \in X$.
Note that we have $\tuple {x, y} \in E$ {{iff}} $x \in E^y$ from the definition of the horizontal section.
In other words: 
:$\paren {f_y}^{-1} \sqbrk E = E^y$
We now show that $f_y$ is $\Sigma_X/\paren {\Sigma_X \otimes \Sigma_Y}$-measurable.
We use Mapping Measurable iff Measurable on Generator.
By the definition of the product $\sigma$-algebra, $\Sigma_X \otimes \Sigma_Y$ is generated by the rectangles $A \times B$ for $A \in \Sigma_X$ and $B \in \Sigma_Y$.  
From Horizontal Section of Cartesian Product, we have:
:$\ds \paren {A \times B}^y = \begin{cases}A & y \in B \\ \O & y \not \in B\end{cases}$
So for each $A \in \Sigma_X$ and $B \in \Sigma_Y$, we have: 
:$\ds \paren {f_y}^{-1} \sqbrk {A \times B} = \begin{cases}A & y \in B \\ \O & y \not \in B\end{cases}$
From the definition of a $\sigma$-algebra, we have:
:$\O \in \Sigma_X$
So we have: 
:$\ds \paren {f_y}^{-1} \sqbrk {A \times B} \in \Sigma_X$
for any $A \in \Sigma_X$ and $B \in \Sigma_Y$. 
So for any $G \in \set {A \times B : A \in \Sigma_X, \, B \in \Sigma_Y}$ we have: 
:$\paren {f_y}^{-1} \sqbrk G \in \Sigma_X$ 
So by Mapping Measurable iff Measurable on Generator:
:$f_y$ is $\Sigma_X/\paren {\Sigma_X \otimes \Sigma_Y}$-measurable.
So, for any $E \in \Sigma_X \otimes \Sigma_Y$ we have: 
:$\paren {f_y}^{-1} \sqbrk E \in \Sigma_X$
So:
:$E^y \in \Sigma_X$
{{qed}}