avewright/proofwiki-math huggingface dataset:
Theorem: Skewness of Geometric Distribution/Formulation 1

:$\map X \Omega = \set {0, 1, 2, \ldots} = \N$
:$\map \Pr {X = k} = \paren {1 - p} p^k$
Then the skewness of $X$ is given by:
:$\gamma_1 = \dfrac {1 + p} {\sqrt p}$

Proof:
From the definition of skewness, we have: 
:$\gamma_1 = \expect {\paren {\dfrac {X - \mu} \sigma}^3}$
where: 
:$\mu$ is the expectation of $X$. 
:$\sigma$ is the standard deviation of $X$.
By Expectation of Geometric Distribution: Formulation 1, we have: 
:$\mu = \dfrac p {1 - p}$
By Variance of Geometric Distribution: Formulation 1, we have: 
:$\sigma = \dfrac {\sqrt p} {1 - p}$ 
So: 
{{begin-eqn}}
{{eqn | l = \gamma_1
      | r = \frac {\expect {X^3 - 3 X^2 \mu + 3 X \mu^2 - \mu^3} } {\sigma^3}
      | c = Cube of Difference
}}
{{eqn | r = \frac {\expect {X^3} - 3 \mu \expect {X^2} + 3 \mu^2 \expect X - \mu^3} {\sigma^3}
      | c = Expectation is Linear
}}
{{eqn | r = \frac {\expect {X^3} - 3 \paren {\dfrac p {1 - p} } \expect {X^2} + 2 \paren {\dfrac {p^3 } {\paren {1 - p}^3} } } {\paren {\dfrac {p \sqrt p} {\paren {1 - p}^3} } } 
      | c = 
}}
{{end-eqn}}
To calculate $\gamma_1$, we must calculate both $\expect {X^2}$ and $\expect {X^3}$.
From Moment in terms of Moment Generating Function:
:$\expect {X^n} = \map { {M_X}^{\paren n} } 0$
where $M_X$ is the moment generating function of $X$.
From Moment Generating Function of Geometric Distribution: Second Moment: 
:$\map { {M_X}' '} t = p \paren {1 - p} e^t \paren {\dfrac {1 + p e^t} {\paren {1 - p e^t}^3} }$
From Moment Generating Function of Geometric Distribution: Third Moment: 
:$\map { {M_X}' ' '} t = p \paren {1 - p } e^t \paren {\dfrac {1 + 4p e^t + p^2 e^{2 t} } {\paren {1 - p e^t}^4 } }$
Setting $t = 0$ and from Exponential of Zero, we have:
:$\map { {M_X}' '} 0 = \dfrac {p \paren {1 + p} } {\paren {1 - p}^2}$
:$\map { {M_X}' ' '} 0 = \dfrac {p \paren {1 + 4 p + p^2} } {\paren {1 - p}^3}$
So:
{{begin-eqn}}
{{eqn | l = \gamma_1
      | r = \frac {\expect {X^3} - 3 \paren {\dfrac p {1 - p} } \expect {X^2} + 2 \paren {\dfrac {p^3} {\paren {1 - p}^3} } } {\paren {\dfrac {p \sqrt p} {\paren {1 - p}^3} } } 
}}
{{eqn | r = \frac {\dfrac {p \paren {1 + 4 p + p^2} } {\paren {1 - p}^3} - 3 \paren {\dfrac p {1 - p} } \dfrac {p \paren {1 + p} } {\paren {1 - p}^2} + 2 \paren {\dfrac {p^3} {\paren {1 - p}^3} } } {\paren {\dfrac {p \sqrt p} {\paren {1 - p}^3} } } 
}}
{{eqn | r = \frac {\paren {1 + 4 p + p^2} - 3 p \paren {1 + p} + 2 p^2} {\sqrt p} 
      | c = $\dfrac p {\paren {1 - p}^3}$ cancels
}}
{{eqn | r = \dfrac {1 + p} {\sqrt p}
}}
{{end-eqn}}
{{qed}}
Category:Skewness of Geometric Distribution
Category:Skewness
dk62lx7uyb456r8y2cdri5x6i3zx94c
Theorem: Excess Kurtosis of Geometric Distribution/Formulation 1

:$\map X \Omega = \set {0, 1, 2, \ldots} = \N$
:$\map \Pr {X = k} = \paren {1 - p} p^k$
Then the excess kurtosis $\gamma_2$ of $X$ is given by: 
:$\gamma_2 = 6 + \dfrac {\paren {1 - p}^2} p$

Proof:
From the definition of excess kurtosis, we have: 
:$\gamma_2 = \expect {\paren {\dfrac {X - \mu} \sigma}^4} - 3$
where: 
:$\mu$ is the expectation of $X$. 
:$\sigma$ is the standard deviation of $X$.
By Expectation of Geometric Distribution: Formulation 1, we have: 
:$\mu = \dfrac p {1 - p}$
By Variance of Geometric Distribution: Formulation 1, we have: 
:$\sigma = \dfrac {\sqrt p } {1 - p}$ 
So: 
{{begin-eqn}}
{{eqn	| l = \gamma_2
	| r = \dfrac {\expect {X^4} - 4 \mu \expect {X^3} + 6 \mu^2 \expect {X^2} - 3 \mu^4} {\sigma^4} - 3
	| c = Kurtosis in terms of Non-Central Moments
}}
{{eqn	| r = \frac {\expect {X^4} - 4 \paren {\dfrac p {1 - p} } \dfrac {p \paren {1 + 4 p + p^2} } {\paren {1 - p}^3 } + 6 \paren {\dfrac p {1 - p} }^2 \dfrac {p \paren {1 + p} } {\paren {1 - p}^2 } - 3 \paren {\dfrac p {1 - p} }^4 } {\paren {\dfrac {\sqrt p } {1 - p} }^4 }  - 3
	| c = Skewness of Geometric Distribution: Formulation 1
}}
{{end-eqn}}
To calculate $\gamma_2$, we must calculate $\expect {X^4}$.
We find this using the moment generating function of $X$, $M_X$. 
From Moment in terms of Moment Generating Function:
:$\expect {X^4} = \map { {M_X}^{\paren 4} } 0$
From Moment Generating Function of Geometric Distribution: Fourth Moment: 
:$\map { {M_X}^{\paren 4} } t = p \paren {1 - p } e^t \paren {\dfrac {1 + 11p e^t + 11 p^2 e^{2t} + p^3 e^{3t} } {\paren {1 - p e^t}^5 } }$
Setting $t = 0$ and from Exponential of Zero, we have:
:$\expect {X^4} = p \paren {\dfrac {1 + 11p + 11 p^2 + p^3 } {\paren {1 - p}^4 } }$
So:
{{begin-eqn}}
{{eqn	| l = \gamma_2
	| r = \frac {\expect {X^4} - 4 \paren {\dfrac p {1 - p} } \dfrac {p \paren {1 + 4 p + p^2} } {\paren {1 - p}^3 } + 6 \paren {\dfrac p {1 - p} }^2 \dfrac {p \paren {1 + p} } {\paren {1 - p}^2 } - 3 \paren {\dfrac p {1 - p} }^4 } {\paren {\dfrac {\sqrt p } {1 - p} }^4 }  - 3
	| c = 
}}
{{eqn	| r = \frac {p \paren {\dfrac {1 + 11p + 11 p^2 + p^3 } {\paren {1 - p}^4 } } - 4 \paren {\dfrac p {1 - p} } \dfrac {p \paren {1 + 4 p + p^2} } {\paren {1 - p}^3 } + 6 \paren {\dfrac p {1 - p} }^2 \dfrac {p \paren {1 + p} } {\paren {1 - p}^2 } - 3 \paren {\dfrac p {1 - p} }^4 } {\paren {\dfrac {\sqrt p } {1 - p} }^4 }  - 3
	| c = 
}}
{{eqn	| r = \frac {\paren {1 + 11p + 11 p^2 + p^3} - 4 \paren {p \paren {1 + 4 p + p^2} } + 6 \paren {p^2 \paren {1 + p} } - 3 p^3 } {p } - 3
        | c = $\dfrac p {\paren {1 - p}^4}$ cancels
}}
{{eqn	| r = \frac {\paren {1 - 4 + 6 - 3} p^3 + \paren {11 - 16 + 6} p^2 + \paren {11 - 4} p + 1} {p } - 3
        | c = 
}}
{{eqn	| r = \frac {p^2 + 7 p + 1} {p } - \frac {3p} p
        | c = 
}}
{{eqn	| r = \frac {6 p + 1 - 2 p + p^2 } {p }
        | c = 
}}
{{eqn	| r = 6 + \dfrac {\paren {1 - p}^2} p
}}
{{end-eqn}}
{{qed}}
Category:Excess Kurtosis of Geometric Distribution
8sac435523q57pj5rx33meptqnd77rq
Theorem: Distributional Derivative of Heaviside Step Function times Cosine

Let $H$ be the Heaviside step function.
Let $\delta$ be the Dirac delta distribution.
Then in the distributional sense:
:$T'_{\map H x \cos x} = T_{- \map H x \sin x} + \delta$

Proof:
$x \stackrel f {\longrightarrow} \map H x \cos x$ is a continuously differentiable real function on $\R \setminus \set 0$ and has a discontinuity at $x = 0$.
By Differentiable Function as Distribution we have that:
:$T'_f = T_{f'}$
Moreover:
:$x < 0 \implies \paren { {\map H x} \map \cos x}' = 0$
:$x > 0 \implies \paren { {\map H x} \map \cos x}' = -\sin x$
Altogether:
:$\forall x \in \R \setminus \set 0 : \paren { {\map H x} \map \cos x}' = - \map H x \sin x$
Furthermore:
:$\map f {0^+} - \map f {0^-} = \map H {0^+} \map \cos {0^+} - \map H {0^-} \map \cos {0^-} = 1$
The result follows from the Jump Rule.
{{qed}}
Theorem: Distributional Derivative of Heaviside Step Function times Sine

Let $H$ be the Heaviside step function.
Let $\delta$ be the Dirac delta distribution.
Then in the distributional sense:
:$T'_{\map H x \sin x} = T_{\map H x \cos x} $

Proof:
$x  \stackrel f {\longrightarrow} \map H x \sin x$ is a continuously differentiable real function on $\R \setminus \set 0$ and possibly has a discontinuity at $x = 0$.
By Differentiable Function as Distribution we have that $T'_f = T_{f'}$.
Moreover:
:$x < 0 \implies \paren { {\map H x} \map \sin x}' = 0$.
:$x > 0 \implies \paren { {\map H x} \map \sin x}' = \cos x$.
Altogether:
:$\forall x \in \R \setminus \set 0 : \paren {{\map H x} \map \sin x}' = \map H x \cos x$
Furthermore:
:$\map f {0^+} - \map f {0^-} = \map H {0^+} \map \sin {0^+} - \map H {0^-} \map \sin {0^-} = 0$
The result follows from the Jump Rule.
{{qed}}
Theorem: Fundamental Solution to 1D Laplace's Equation

Let $\ds \map f x = \frac {\size x} 2$ where $\size x$ is the absolute value function.
Let $\delta \in \map {\DD'} \R$ be the Dirac delta distribution.
Let $T_f \in \map {\DD'} \R$ be the Schwartz distribution associated with $f$.
Then $T_f$ is the fundamental solution to the $1$-dimensional Laplace's equation.
That is:
:$T' '_f = \delta$
or in the distributional sense:
:$\dfrac {\d^2} {\d x^2} f = \delta$

Proof:
$x \stackrel f {\longrightarrow} \dfrac {\size x} 2$ is a continuously differentiable real function on $\R \setminus \set 0$ and possibly has a discontinuity at $x = 0$.
By Differentiable Function as Distribution we have that $T'_f = T_{f'}$.
Moreover:
:$x < 0 \implies \paren {\dfrac {\size x} 2}' = -\frac 1 2$
:$x > 0 \implies \paren {\dfrac {\size x} 2}' = \frac 1 2$
Altogether:
:$\forall x \in \R \setminus \set 0 : \paren {\dfrac {\size x} 2}' = \map g x$
where:
:$\map g x = \begin {cases} \dfrac 1 2 & : x > 0 \\ -\dfrac 1 2 & : x < 0 \end {cases}$
Furthermore:
:$\map f {0^+} - \map f {0^-} = 0$
By the Jump Rule:
:$T'_f = T_g$
$x \stackrel g {\longrightarrow} \map g x$ is a continuously differentiable real function on $\R \setminus \set 0$ and possibly has a discontinuity at $x = 0$.
By similar arguments:
:$\forall x \in \R \setminus \set 0 : \map {g'} x = 0$
Furthermore:
:$\map g {0^+} - \map g {0^-} = 1$
By the Jump Rule:
:$T'_g = \delta$
By the definition of distributional derivative:
{{begin-eqn}}
{{eqn | l = T' '_f
      | r = \paren {T'_f}'
}}
{{eqn | r = T'_{f'}
}}
{{eqn | r = T'_g
}}
{{eqn | r = \delta
}}
{{end-eqn}}
Hence, if $\map f x = \dfrac {\size x} 2$, then $T' '_f = \delta$.
{{qed}}
Theorem: Minimal Element need not be Unique

Let $\struct {S, \preccurlyeq}$ be an ordered set.
It is possible for $S$ to have more than one minimal element.

Proof:
Proof by Counterexample:
Consider the set $S$ defined as:
:$S = \N \setminus \set {0, 1}$
That is, $S$ is the set of natural numbers with $0$ and $1$ removed.
Let $\preccurlyeq$ be the ordering on $S$ defined as:
:$\forall a, b \in S: a \preccurlyeq b \iff a \divides b$
where $a \divides b$ denotes that $a$ is a divisor of $b$.
From Divisor Relation on Positive Integers is Partial Ordering, $\struct {S, \preccurlyeq}$ is a partially ordered set.
Let $p \in S$ be a prime number.
Let $a \divides p$.
By definition of prime number, the only divisors of $p$ are $-p$, $-1$, $1$ and $p$.
Of these, only $p$ is an element of $S$.
Hence if $a \divides p$ it must be the case that $a = p$.
Hence $p$ is a minimal element of $S$ by definition.
Thus every prime number is a minimal element of $S$.
The result follows.
{{qed}}
Theorem: Maximal Element need not be Unique

Let $\struct {S, \preccurlyeq}$ be an ordered set.
It is possible for $S$ to have more than one maximal element.

Proof:
Proof by Counterexample:
Consider the set $T$ defined as:
:$T = \set {0, 1}$
Let $S$ be defined as:
:$S := \powerset T \setminus T$
where $\powerset T$ denotes the power set of $T$.
That is:
:$S = \set {\O, \set 0, \set 1}$
Let $\preccurlyeq$ be the relation defined on $S$ as:
:$\forall a, b \in S: a \preccurlyeq b \iff a \subseteq b$
That is, $\preccurlyeq$ is the subset relation on $S$.
From Subset Relation is Ordering, $\struct {S, \preccurlyeq}$ is an ordered set.
Let $a \in S$ such that $\set 1 \preccurlyeq a$.
Then by inspection it is apparent that:
:$a = \set 1$
That is, $\set 1$ is a maximal element of $\struct {S, \preccurlyeq}$.
Similarly, let $a \in S$ such that $\set 0 \preccurlyeq a$.
Then by inspection it is apparent that:
:$a = \set 0$
That is, $\set 0$ is also a maximal element of $\struct {S, \preccurlyeq}$.
Hence $S$ has more than one maximal element.
{{qed}}
Theorem: Ordered Set may not have Minimal Element

Let $\struct {S, \preccurlyeq}$ be an ordered set.
It may be the case that $S$ has no minimal elements.

Proof:
Let $\Q_{>0}$ denote the set of (strictly) positive rational numbers.
From Rational Numbers form Totally Ordered Field, the rational numbers $\Q$ are totally ordered by the usual ordering $\le$.
From Subset of Toset is Toset, $\Q_{>0}$ is also totally ordered by $\le$.
Thus $\struct {\Q_{>0}, \le}$ is an ordered set.
{{AimForCont}} there exists a minimal element $m$ of $\struct {\Q_{>0}, \le}$.
From Minimal Element in Toset is Unique and Smallest, $m$ is also the smallest element of $\struct {\Q_{>0}, \le}$
By Smallest Strictly Positive Rational Number does not Exist, $\struct {\Q_{>0}, \le}$ has no smallest element.
Hence $m$ cannot be a minimal element of $\struct {\Q_{>0}, \le}$.
It follows by Proof by Contradiction that $\struct {\Q_{>0}, \le}$ has no minimal elements.
{{qed}}
Theorem: Ordered Set may not have Maximal Element

Let $\struct {S, \preccurlyeq}$ be an ordered set.
It may be the case that $S$ has no maximal elements.

Proof:
Consider the set $S$ defined as:
:$S = \N \setminus \set 0$
That is, $S$ is the set of natural numbers with $0$ removed.
Let $\preccurlyeq$ be the ordering on $S$ defined as:
:$\forall a, b \in S: a \preccurlyeq b \iff a \divides b$
where $a \divides b$ denotes that $a$ is a divisor of $b$.
From Divisor Relation on Positive Integers is Partial Ordering, $\struct {S, \preccurlyeq}$ is a partially ordered set.
{{AimForCont}} $S$ has a maximal element $m$.
Consider the natural number $n = 2 m$.
Then:
:$m \divides n$
but:
:$m \ne n$
and so by definition $m$ is not a maximal element of $S$.
Hence by Proof by Contradiction it follows that there exists no such $m$.
Hence the result.
{{qed}}
Theorem: Distributional Derivatives of Dirac Delta Distribution do not Vanish

Let $\delta \in \map {\DD'} \R$ be the Dirac delta distribution.
Then for any $n \in \N$ the distributional derivative $\delta^{\paren n}$ does not vanish.

Proof:
Let $\phi \in \map \DD \R$ be a test function such that $\map \phi 0 \ne 0$.
Then:
:$\forall n \in \N : \forall x \in \R : x^n \phi \in \map \DD \R$
By the definition of the distributional derivative:
{{begin-eqn}}
{{eqn | l = \map {\delta^{\paren n} } {x^n \phi}
      | r = \paren {-1}^n \map \delta {\paren {x^n \phi}^{\paren n} }
}}
{{eqn | r = \paren {-1}^n \map \delta {\sum_{k \mathop = 0}^n \binom n k \paren {\dfrac {\d^k} {\d x^k} x^n} \phi^{\paren {n - k} } }
      | c = Leibniz's Rule in One Variable
}}
{{eqn | r = \paren {-1}^n \binom n n n! \map \phi 0
      | c = Nth Derivative of Nth Power, {{Defof|Dirac Delta Distribution}}
}}
{{eqn | o = \ne
      | r = 0
}}
{{end-eqn}}
{{qed}}
Theorem: Expectation of Logistic Distribution

Let $X$ be a continuous random variable which satisfies the logistic distribution:
:$X \sim \map {\operatorname {Logistic} } {\mu, s}$
The expectation of $X$ is given by:
:$\expect X = \mu$

Proof:
From the definition of the logistic distribution, $X$ has probability density function:
:$\map {f_X} x = \dfrac {\map \exp {-\dfrac {\paren {x - \mu} } s} } {s \paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^2}$
From the definition of the expected value of a continuous random variable: 
:$\ds \expect X = \int_{-\infty}^\infty x \, \map {f_X} x \rd x$
So:
:$\ds \expect X = \frac 1 s \int_{-\infty}^\infty \dfrac {x \map \exp {-\dfrac {\paren {x - \mu} } s} } {\paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^2} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^{-1}
      | c = Integration by Substitution
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = -\paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^{-2} \paren {-\frac 1 s \map \exp {-\dfrac {\paren {x - \mu} } s} }
      | c = Power Rule for Derivatives, Chain Rule for Derivatives and {{Corollary|Derivative of Exponential Function|1}}
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 u - 1
      | r = \paren {\map \exp {-\dfrac {\paren {x - \mu} } s} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\dfrac 1 u - 1}
      | r = -\dfrac {\paren {x - \mu} } s
      | c =
}}
{{eqn | ll= \leadsto
      | l = -s \map \ln {\dfrac {1 - u} u} + \mu
      | r = x
      | c =
}}
{{end-eqn}}
and also:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to -\infty} \paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^{-1}
      | r = 0
      | c = 
}}
{{eqn | l = \lim_{x \mathop \to \infty} \paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^{-1}
      | r = 1
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn	| l = \expect X
        | r = \int_{\to 0}^{\to 1}  \paren {-s \map \ln {\dfrac {1 - u} u} + \mu} \rd u
	| c = 
}}
{{eqn	| r = -s \int_{\to 0}^{\to 1} \map \ln {\dfrac {1 - u} u} \rd u + \mu \int_{\to 0}^{\to 1} \rd u
	| c = 
}}
{{eqn	| r = -s \paren {\int_{\to 0}^{\to 1} \map \ln {1 - u} \rd u - \int_{\to 0}^{\to 1} \map \ln u \rd u} + \mu
        | c = Integral of Constant and Difference of Logarithms
}}
{{eqn	| r = -s \paren {\paren {-1} - \paren {-1} } + \mu
        | c = {{Lemma|Expectation of Logistic Distribution|1}} and {{Lemma|Expectation of Logistic Distribution|2}}
}}
{{eqn	| r = \mu
	| c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Expectation of Logistic Distribution

Let $X$ be a continuous random variable which satisfies the logistic distribution:
:$X \sim \map {\operatorname {Logistic} } {\mu, s}$
The expectation of $X$ is given by:
:$\expect X = \mu$

Proof:
By Moment Generating Function of Logistic Distribution, the moment generating function of $X$ is given by: 
:$\ds \map {M_X} t = \map \exp {\mu t} \int_{\to 0}^{\to 1} \paren {\dfrac {1 - u} u}^{-s t} \rd u$
for $\size t < \dfrac 1 s$. 
From Moment in terms of Moment Generating Function: 
:$\expect X = \map { {M_X}'} 0$
From Moment Generating Function of Logistic Distribution: First Moment: 
:$\ds \map { {M_X}'} t = \map \exp {\mu t} \paren {\mu \int_{\to 0}^{\to 1} \paren {\dfrac {1 - u} u}^{-s t} \rd u - s \int_{\to 0}^{\to 1} \map \ln {\dfrac {1 - u} u} \paren {\dfrac {1 - u} u}^{-s t} \rd u}$
Hence setting $t = 0$:
{{begin-eqn}}
{{eqn | l = \map { {M_X}'} 0
      | r = \mu \int_{\to 0}^{\to 1} \rd u - s \int_{\to 0}^{\to 1} \map \ln {\dfrac {1 - u} u} \rd u
}}
{{eqn | r = \mu - s \paren {0 }
      | c = Definite Integral of Constant and {{Lemma|Expectation of Logistic Distribution|3}}
}}
{{eqn | r = \mu
}}
{{end-eqn}}
{{qed}}
Theorem: Ordered Set with Multiple Minimal Elements has no Smallest Element

Let $\struct {S, \preccurlyeq}$ be an ordered set.
Let $\struct {S, \preccurlyeq}$ have more than one minimal element.
Then $\struct {S, \preccurlyeq}$ has no smallest element.

Proof:
Let $s$ and $t$ both be minimal elements of $\struct {S, \preccurlyeq}$ such that $s \ne t$.
Then by definition:
:$\forall x \in S: x \preccurlyeq s \implies s = x$
and:
:$\forall x \in S: x \preccurlyeq t \implies t = x$
{{AimForCont}} $S$ has a smallest element $m$.
Then by definition:
:$\forall y \in S: m \preccurlyeq y$
Hence:
:$m \preccurlyeq s$
and also:
:$m \preccurlyeq t$
But because $s$ and $t$ are both minimal elements of $\struct {S, \preccurlyeq}$:
:$s = m$
and:
:$t = m$
This contradicts the fact that $s \ne t$.
Hence by Proof by Contradiction there can be no smallest element of $\struct {S, \preccurlyeq}$.
{{qed}}
Category:Minimal Elements
Category:Smallest Elements
506q1modh350dz9cm8xfyhqwg9blf34
Theorem: Ordered Set with Multiple Maximal Elements has no Greatest Element

Let $\struct {S, \preccurlyeq}$ be an ordered set.
Let $\struct {S, \preccurlyeq}$ have more than one maximal element.
Then $\struct {S, \preccurlyeq}$ has no greatest element.

Proof:
Let $s$ and $t$ both be maximal elements of $\struct {S, \preccurlyeq}$ such that $s \ne t$.
Then by definition:
:$\forall x \in S: s \preccurlyeq x \implies s = x$
and:
:$\forall x \in S: t \preccurlyeq x \implies t = x$
{{AimForCont}} $S$ has a greatest element $m$.
Then by definition:
:$\forall y \in S: y \preccurlyeq m$
Hence:
:$s \preccurlyeq m$
and also:
:$y \preccurlyeq m$
But because $s$ and $t$ are both maximal elements of $\struct {S, \preccurlyeq}$:
:$s = m$
and:
:$t = m$
This contradicts the fact that $s \ne t$.
Hence by Proof by Contradiction there can be no greatest element of $\struct {S, \preccurlyeq}$.
{{qed}}
Category:Maximal Elements
Category:Greatest Elements
8haop32c4qkt6n4tl9tw678j16wd9cm
Theorem: Unique Minimal Element may not be Smallest

Let $\struct {S, \preccurlyeq}$ be an ordered set.
Let $\struct {S, \preccurlyeq}$ have a unique minimal element.
Then it is not necessarily the case that $\struct {S, \preccurlyeq}$ has a smallest element.

Proof:
Let $S$ be the set defined as:
:$S = \Z \cup \set m$
where:
:$\Z$ denotes the set of integers
:$m$ is an arbitrary object such that $m \ne \Z$.
Let $\preccurlyeq$ be the relation on $\Z$ defined as:
:$\forall a, b \in S: a \preccurlyeq b \iff \begin {cases} a \le b & : a, b \in \Z \\ a = m = b & : a, b \notin \Z \end{cases}$
where $\le$ is the usual ordering on $\Z$.
Note that for all $x \in \Z$, we have that $x$ and $m$ are non-comparable.
Then $\struct {S, \preccurlyeq}$ is an ordered set such that:
:$m$ is the only minimal element of $\struct {S, \preccurlyeq}$
:$\struct {S, \preccurlyeq}$ has no smallest element.
This is shown as follows:
Let $x \in S$ such that $x \preccurlyeq m$.
Then by definition $x = m$.
Hence $m$ is a minimal element of $\struct {S, \preccurlyeq}$.
{{AimForCont}} $y \in \Z$ is another minimal element of $\struct {S, \preccurlyeq}$.
Let $z = y - 1$.
By definition of $\Z$, we have that $z \in \Z$.
But $z \le y$ and so $z \preccurlyeq y$.
Hence for all $y \in \Z$, it is not the case that $y$ is a minimal element of $\struct {S, \preccurlyeq}$.
Hence by Proof by Contradiction it follows that the minimal element $m$ of $\struct {S, \preccurlyeq}$ is unique.
{{AimForCont}} $x \in S$ is the smallest element of $\struct {S, \preccurlyeq}$.
Suppose $x \in \Z$.
Then because $x$ and $m$ are non-comparable, it is not the case that $x \preccurlyeq m$.
Hence $x$ cannot be the smallest element.
Suppose $x = m$.
Let $a \in S: a \ne m$.
Then $x$ and $a$ are again non-comparable.
Hence it is not the case that $x \preccurlyeq a$.
Hence $x$ again cannot be the smallest element of $\struct {S, \preccurlyeq}$.
So by Proof by Cases $x$ cannot be the smallest element of $\struct {S, \preccurlyeq}$.
It follows by Proof by Contradiction that there can be no smallest element of $\struct {S, \preccurlyeq}$.
{{qed}}
Theorem: Equivalence of Definitions of Well-Founded Relation

Let $\struct {S, \RR}$ be a Relational Structure.
{{TFAE|def = Well-Founded Relation}}

Proof:
By definition of minimal element:
:$\forall y \in T: y \preceq x \implies x = y$
Theorem: Strictly Minimal Element is Minimal Element

Let $\struct {S, \RR}$ be a relational structure.
Let $T \subseteq S$ be a subset of $S$.
Let $m \in T$ be a strictly minimal element of $T$ under $\RR$.
Then $m$ is a minimal element of $T$ under $\RR$.

Proof:
Let $m \in T$ be a strictly minimal element of $T$ under $\RR$.
Then by definition:
:$\forall x \in T: \tuple {x, m} \notin \RR$
{{AimForCont}} $m$ is not a minimal element of $T$ under $\RR$.
Then:
:$\exists y \in T: \tuple {y, m} \in \RR$
such that $y \ne m$.
But this contradicts the assertion that $\tuple {y, m} \notin \RR$.
Hence it cannot be the case that $m$ is not a minimal element of $T$ under $\RR$.
That is:
:$m$ is a minimal element of $T$ under $\RR$.
{{qed}}
Category:Minimal Elements
cjl7lebyjovxugxi83f6zj9ai8zzude
Theorem: Strictly Maximal Element is Maximal Element

Let $\struct {S, \RR}$ be a relational structure.
Let $T \subseteq S$ be a subset of $S$.
Let $m \in T$ be a strictly maximal element of $T$ under $\RR$.
Then $m$ is a maximal element of $T$ under $\RR$.

Proof:
Let $m \in T$ be a strictly maximal element of $T$ under $\RR$.
Then by definition:
:$\forall x \in T: \tuple {m, x} \notin \RR$
{{AimForCont}} $m$ is not a maximal element of $T$ under $\RR$.
Then:
:$\exists y \in T: \tuple {m, y} \in \RR$
such that $y \ne m$.
But this contradicts the assertion that $\tuple {m, y} \notin \RR$.
Hence it cannot be the case that $m$ is not a maximal element of $T$ under $\RR$.
That is:
:$m$ is a maximal element of $T$ under $\RR$.
{{qed}}
Category:Maximal Elements
atmhil3tvtkrpykxyx75sh2ozhjwjd2
Theorem: Strictly Well-Founded Relation is Well-Founded

Let $\struct {S, \RR}$ be a relational structure.
Let $\RR$ be a strictly well-founded relation on $S$.
Then $\RR$ is a well-founded relation on $S$.

Proof:
We have that $\RR$ is a strictly well-founded relation on $S$.
By definition:
:$\forall T: \paren {T \subseteq S \land T \ne \O} \implies \exists y \in T: \forall z \in T: \neg \paren {z \mathrel \RR y}$
It immediately follows that:
:$\forall T: \paren {T \subseteq S \land T \ne \O} \implies \exists y \in T: \forall z \in \paren {T \setminus \set y}: \neg \paren {z \mathrel \RR y}$
which is the definition of a well-founded relation on $S$.
{{qed}}