nyuuzyou/wikis huggingface dataset:
Induction of Finite Set

== Theorem Scheme ==
Let $A$ be finite set.
Let $\map P -$ be a predicate.
Let $\map P \O$.
Let
:$\forall B \subseteq A, x \in A: \paren {\map P B \implies \map P {B \cup \set x} }$
Then:
:$\map P A$
== Proof ==
We will prove the result by induction on cardinality of argument.
=== Base Case ===
:$\forall X \subseteq A: \paren {\size X = 0 \implies \map P X}$
Let $X \subseteq A$ such that:
:$\size X = 0$
By Cardinality of Empty Set:
:$X = \O$
Thus by assumption:
:$\map P X$
=== Induction Hypothesis ===
:$\forall X \subseteq A: \paren {\size X = n \implies \map P X}$
=== Induction Step ===
:$\forall X \subseteq A: \paren {\size X = n + 1 \implies \map P X}$
Let $X \subseteq A$ such that:
:$\size X = n + 1$
By definition of cardinality:
:$X = \set {x_1, \dots, x_n, x_{n + 1} }$
By Union of Unordered Tuples:
:$X = \set {x_1, \dots, x_n} \cup \set {x_{n + 1} }$
By definition of cardinality:
:$\size {\set {x_1, \dots, x_n} } = n$
By Set is Subset of Union:
:$\set {x_1, \dots, x_n} \subseteq X \subseteq A$
Then by Induction Hypothesis:
:$\map P {\set {x_1, \dots, x_n} }$
By definition of subset:
:$x_{n + 1} \in A$
Thus by assumption:
:$\map P X$
By the Principle of Mathematical Induction:
:$\forall X \subseteq A: \paren {\size X = \size A \implies \map P X}$
Hence:
:$\map P A$
== Sources ==
* 
Category:Set Theory
Induction on Well-Formed Formulas

== Theorem ==
Let $\FF$ be a formal language with a bottom-up grammar.
Let $\Phi$ be a proposition about the well-formed formulas of $\FF$.
Suppose that $\Phi$ is true for all letters of $\FF$.
Suppose further that every rule of formation preserves $\Phi$, i.e. when fed well-formed formulas satisfying $\Phi$, it yields new well-formed formulas satisfying $\Phi$.
Then all well-formed formulas of $\FF$ satisfy $\Phi$.
== Proof ==
By definition of bottom-up grammar, the well-formed formulas of $\FF$ comprise:
:letters of $\FF$;
:expressions resulting from rules of formation.
Either case is dealt with by the assumptions on $\Phi$.
Hence the result, from Proof by Cases.
Category:Formal Languages
Inductive Construction of Natural Numbers fulfils Peano's Axiom of Injectivity

== Theorem ==
Let $P$ denote the set of natural numbers by definition as an inductive set.
Then $P$ fulfils:
:
where $s$ denotes the successor mapping.
== Proof ==
Let $m$ and $n$ be natural numbers such that $n^+ = m^+$.
By construction:
:$n \in n^+$
and:
:$m \in m^+$
Thus as $n^+ = m^+$ we have:
:$n \in m^+$
and:
:$m \in n^+$
This gives us:
:$n \in m \lor n = m$
and:
:$m \in n \lor m = n$
 that $n \ne m$.
Then from $n \in m \lor n = m$ we have:
:$n \in m$
and from $m \in n \lor m = n$ we have:
:$m \in n$
In summary, if $n \ne m$ we have 
:$n \in m$ and $m \in n$
But from Natural Numbers cannot be Elements of Each Other, this is not possible.
Hence by Proof by Contradiction:
:$n^+ = m^+ \implies n = m$
and the result follows by definition of injection.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 3$ Derivation of the Peano postulates and other results
Category:Peano's Axioms
Category:Inductive Sets
Category:Natural Numbers
Inductive Construction of Natural Numbers fulfils Peano's Axioms

== Theorem ==
Let $P$ denote the set of natural numbers by definition as an inductive set.
Then $P$ fulfils Peano's axioms.
== Proof ==
By definition of inductive set:
:$\O \in P$
By definition of the natural numbers, $\O$ is identified with $0$ (zero).
Thus holds.
Let $x$ be a natural number.
By definition, $x$ is an element of every inductive set.
Thus if $x \in P$ it follows that $x^+ \in P$.
Thus holds.
By Inductive Construction of Natural Numbers fulfils Peano's Axiom of Injectivity, holds.
For all $n$, $n$ is an element of $n^+$.
But $0$ is identified with the empty set $\O$.
By definition, $\O$ has no elements.
Therefore it is not possible for $\O$ to equal $n^+$ for any $n$.
Thus holds.
 holds immediately by definition of inductive set.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 3$ Derivation of the Peano postulates and other results
Category:Peano's Axioms
Category:Inductive Sets
Category:Natural Numbers
Inductive Construction of Sigma-Algebra Generated by Collection of Subsets/Corollary

== Corollary to Inductive Construction of Sigma-Algebra Generated by Collection of Subsets ==
Let $\EE$ be a set of sets which are subsets of some set $X$.
Let $\map \sigma \EE$ be the $\sigma$-algebra generated by $\EE$.
Let the cardinality of $\EE$ satisfy:
:$\size \N \le \size \EE \le \mathfrak c$
where $\mathfrak c$ denotes the cardinality of the continuum.
Then:
:$\size {\map \sigma \EE} = \mathfrak c$
== Proof ==
By Inductive Construction of Sigma-Algebra Generated by Collection of Subsets:
:$\ds \bigcup_{\alpha \mathop \in \Omega} \EE_{\alpha} = \map \sigma \EE$
Thus by Leibniz's Law:
:$\size {\ds \bigcup_{\alpha \mathop \in \Omega} \EE_{\alpha} } = \size {\map \sigma \EE}$
By the definition of union:
:$\EE_\alpha \subseteq \map \sigma \EE$ for all $\alpha \in \Omega$.
Thus:
:$\size {\EE_\alpha} \le \size {\map \sigma \EE}$ for all $\alpha \in \Omega$.
By Corollary of Existence of Minimal Uncountable Well-Ordered Set:
:$\size \Omega \le \mathfrak c$
By Cardinality of Infinite Union of Infinite Sets:
:$\ds \size {\bigcup_{\alpha \mathop \in \Omega} \EE_{\alpha} } \le \mathfrak c$
Thus:
:$\size {\map \sigma \EE} \le \mathfrak c$
By Cardinality of Infinite Sigma-Algebra is at Least Cardinality of Continuum:
:$\size {\map \sigma \EE} \ge \mathfrak c$
The result follows from the Cantor-Bernstein-Schröder Theorem.
== Sources ==
* : $\S 1.23$
Category:Sigma-Algebras
Inductive Definition of Sequence

== Theorem ==
Let $X$ be a set.
Let $h \in \N$.
Let $a_i \in X$ for all $i \in \set {1, 2, \ldots, h}$.
Let $S$ be the set of all finite sequences whose codomains are in $X$.
Let $G: S \to X$ be a mapping.
Then there is a unique sequence $f$ whose codomain is in $X$ such that:
:$f_i = \begin{cases} a_i & : i \in \set {1, 2, \ldots, h} \\ \map G {f_1, f_2, \ldots, f_{i - 1} } & : i \ge h + 1 \end{cases}$
== Proof ==
== Also known as ==
Such a definition for a sequence is also known as a recursive definition.
== Sources ==
* : $\S 1.18$: Sequences Defined Inductively: Theorem $18.4$
* : Appendix $\text{A}.12$: Induction
Category:Mapping Theory
Inductive Semigroup whose Inductive Elements Commute is Commutative Semigroup

== Theorem ==
Let $\struct {S, \circ}$ be a semigroup.
Let there exist $\alpha, \beta \in S$ which fulfil the condition for $\struct {S, \circ}$ to be an inductive semigroup:
:the only subset of $S$ containing both $\alpha$ and $x \circ \beta$ whenever it contains $x$ is $S$ itself.
Let $\alpha$ and $\beta$ commute.
Then $\struct {S, \circ}$ is a commutative semigroup.
== Proof ==
Suppose $\struct {S, \circ}$ is a semigroup.
Suppose there exist $\alpha, \beta \in S$ such that $\struct {S, \circ}$ is an inductive semigroup. 
That is, suppose there exist $\alpha, \beta \in S$ such that the only subset of $S$ containing both $\alpha$ and $x \circ \beta$ whenever it contains $x$ is $S$ itself.
That is:
:$\exists \alpha, \beta \in S: \forall A \subseteq S: \paren {\alpha \in A \land \paren {\forall x \in A: x \circ \beta \in A} } \implies A = S$
By Form of Elements of Inductive Semigroup, the elements of $S$ are of the form:
:$\alpha \circ \beta \circ \beta \circ \cdots \circ \beta$
Then:
:$\forall x, y \in S: x \circ y = y \circ x$
Hence, $\struct {S, \circ}$ is a commutative semigroup, as required.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 16$: The Natural Numbers: Exercise $16.9 \ \text {(a)}$
Category:Inductive Semigroups
Category:Commutative Semigroups
Inductive Set under Mapping has Minimally Inductive Subset

== Theorem ==
Let $A$ be an inductive class under a mapping $g$.
Let $A$ be a set.
Then there exists some subset $S$ of $A$ such that $S$ is minimally inductive under $g$.
== Proof ==
Let $S$ be the set defined as:
:$S = \set {s: \exists t \in A: t = \map g s} \cup \set \O$
By definition, we have that:
:$\O \in S$
:$s \in S \implies \map g s \in S$
So, by definition, $S$ is inductive under $g$.
Because $A$ is inductive under $g$:
:$\O \in A$
and so by definition of subset:
:$S \subseteq A$
It remains to be shown that $S$ is minimally inductive under $g$.
Let $T \subseteq S$ such that $T$ is inductive under $g$.
It will be demonstrated by the Principle of General Induction that $T = S$.
That is:
:$\forall x \in T: x \in S$
Let $P: T \to \set {\T, \F}$ be the propositional function defined as:
:$\forall x \in T: \map P x \iff x \in S$
First it is noted that as $T$ is inductive under $g$:
:$\O \in T$
But $\O \in S$.
Hence we have that:
:$\map P \O = \T$
This is the basis for the induction.
Now suppose $x \in T$ such that $\map P x = \T$.
That is:
:$x \in S$
This is the induction hypothesis.
The induction step is to show that $\map P {\map g x} = \T$.
That is:
:$\map g x \in S$
Indeed, as $T$ is inductive under $g$:
:$x \in T \implies \map g x \in T$
But again, :
:$\map g x \in S$
Hence we have shown that:
:$\map P x = \T \implies \map P {\map g x} = \T$
Hence it follows by the Principle of General Induction:
:$\forall x \in T: \map P x = \T$
That is:
:$\forall x \in T: x \in S$
That is:
:$T = S$
Thus a subset of $S$ which is inductive under $g$ is necessarily equal to $S$.
Hence $S$ has no proper subset which is inductive under $g$.
Hence, by definition, $S$ is minimally inductive under $g$.
The result follows.
== Sources ==
* : Chapter $3$: The Natural Numbers: $\S 4$ A double induction principle and its applications: Exercise $4.2$
Category:Inductive Classes
Category:Proofs by Induction
Category:Minimally Inductive Classes
Inequalities Concerning Roots

== Theorem ==
Let $\closedint X Y$ be a closed real interval such that $0 < X \le Y$.
Let $x, y \in \closedint X Y$.
Then:
:$\forall n \in \N_{> 0}: X Y^{1/n} \size {x - y} \le n X Y \size {x^{1/n} - y^{1/n} } \le Y X^{1/n} \size {x - y}$
== Proof ==
From Difference of Two Powers:
:$\ds a^n - b^n = \paren {a - b} \paren {a^{n - 1} + a^{n - 2} b + a^{n - 3} b^2 + \dotsb + a b^{n - 2} + b^{n - 1} } = \paren {a - b} \sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} b^j$
Let $a > b > 0$.
Then:
:$\dfrac {a^n - b^n} {a - b} = a^{n - 1} + a^{n - 2} b + a^{n - 3} b^2 + \dotsb + a b^{n - 2} + b^{n - 1}$
Also, note that:
:$b^{n - 1} = b^{n - j - 1} b^j \le a^{n - j - 1} b^j \le a^{n - j -1} a^j \le a^{n - 1}$
Hence if $a > b > 0$:
:$n b^{n - 1} \le \dfrac {a^n - b^n} {a - b} \le n a^{n - 1}$
Taking reciprocals:
:$\dfrac 1 {n b^{n - 1} } \ge \dfrac {a - b} {a^n - b^n} \ge \dfrac 1 {n a^{n - 1} }$
Thus:
:$\dfrac {a^n - b^n} {n a^{n - 1} } \le a - b \le \dfrac {a^n - b^n} {n b^{n - 1} } \implies \dfrac {a \paren {a^n - b^n} } {a^n} \le n \paren {a - b} \le \dfrac {b \paren {a^n - b^n} } {b^n}$
Now suppose $x > y$.
Then:
:$x - y = \size {x - y}$
and:
:$x^{1/n} - y^{1/n} = \size {x^{1/n} - y^{1/n} }$
Then put $a = x^{1/n}$ and $b = y^{1/n}$ in the above:
:$\dfrac {x^{1/n} \size {x - y} } x \le n \size {x^{1/n} - y^{1/n} } \le \dfrac {y^{1/n} \size {x - y} } y$
Multiplying through by $x y$:
:$x^{1/n} y \size {x - y} \le n x y \size {x^{1/n} - y^{1/n} } \le x y^{1/n} \size {x - y}$
Similarly, if $y > x$:
:$y^{1/n} x \size {x - y} \le n x y \size {x^{1/n} - y^{1/n} } \le y x^{1/n} \size {x - y}$
The result follows after some algebra.
== Sources ==
* : $\S 3$: Natural Numbers: Exercise $\S 3.11 \ (6)$
Category:Roots of Numbers
Category:Inequalities
Inequality Rule for Absolutely Convergent Generalized Sums

== Theorem ==
Let $V$ be a Banach space.
Let $\family {v_i}_{i \mathop \in I}$ be an indexed family of elements of $V$.
Let the generalized sum $\ds \sum \set {v_i: i \in I}$ be absolutely net convergent.
Let $\family {w_i}_{i \mathop \in I}$ be an indexed family of elements of $V$:
:$\forall i \in I : \norm{w_i} \le \norm{v_i}$
Then:
:the generalized sum $\ds \sum_{i \mathop \in I} \norm{w_i}$ is absolutely net convergent
and:
:$\ds \sum_{i \mathop \in I} \norm{w_i} \le \sum_{i \mathop \in I} \norm{v_i}$
== Proof ==
By definition of absolutely net convergence, let:
:$\ds \sum_{i \mathop \in I} \norm{v_i} = M$
Let $F \subseteq I$ be finite.
From Absolutely Convergent Generalized Sum Converges to Supremum:
:$\ds \sum_{i \mathop \in F} \norm{v_i} \le M$
So :
:$\ds \sum_{i \mathop \in F} \norm{w_i} \le \ds \sum_{i \mathop \in F} \norm{v_i} \le M$
Since $F \subseteq J$ was arbitrary, it follows that:
:$\forall F \subseteq F : F$ is finite $: \ds \sum_{i \mathop \in F} \norm{w_i} \le M$
From Bounded Generalized Sum is Absolutely Convergent:
:$\ds \sum_{i \mathop \in I} \norm{w_i}$ is absolutely net convergent
From Inequality Rule for Real Convergent Nets:
:$\ds \sum_{i \mathop \in I} \norm{w_i} \le \sum_{i \mathop \in I} \norm{v_i}$
Category:Banach Spaces
Category:Generalized Sums
Inequality Rule for Real Convergent Nets

== Theorem == 
Let $\struct {\Lambda, \preceq}$ be a directed set.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ and $\family {y_\lambda}_{\lambda \mathop \in \Lambda}$ be indexed families of elements in $\R$.
Let $\family {x_\lambda}_{\lambda \mathop \in \Lambda}$ and $\family {y_\lambda}_{\lambda \mathop \in \Lambda}$ be convergent to the following limits:
:$\ds \lim_{\lambda \mathop \in \Lambda} x_\lambda = l$
:$\ds \lim_{\lambda \mathop \in \Lambda} y_\lambda = m$
Let there exist $\lambda \in \Lambda$ such that:
:$\forall \mu \in \Lambda : \lambda \preceq \mu: x_\mu \le y_\mu$
Then:
:$l \le m$
== Proof ==
:$l > m$
Let $\epsilon = \dfrac {\paren{l - m}} 2$.
Hence:
:$\epsilon > 0$
and:
:$(1) \quad l - \epsilon = m + \epsilon$ 
By definition of convergence:
:$\exists \lambda_1 \in \Lambda : \forall \mu \in \Lambda : \lambda_1 \preceq \mu \implies \size{l - x_\mu} < \epsilon$
and:
:$\exists \lambda_2 \in \Lambda : \forall \mu \in \Lambda : \lambda_2 \preceq \mu \implies \size{m - y_\mu} < \epsilon$
From Closed Interval Defined by Absolute Value:
:$(2) \quad \forall \mu \in \Lambda : \lambda_1 \preceq \mu \implies l - \epsilon < x_\mu$
and:
:$(3) \quad \forall \mu \in \Lambda : \lambda_2 \preceq \mu \implies m + \epsilon > y_\mu$
By definition of directed set:
:$\exists \mu \in \Lambda : \lambda, \lambda_1, \lambda_2 \preceq \mu$
We have:
This contradicts the hypothesis:
:$\forall \mu \in \Lambda : \lambda \preceq \mu: x_\mu \le y_\mu$
Hence:
:$l \le m$
Category:Nets (Set Theory)
Inequality Rule for Real Sequences

== Theorem == 
Let $\sequence {x_n}$ and $\sequence {y_n}$ be sequences in $\R$.
Let $\sequence {x_n}$ and $\sequence {y_n}$ be convergent to the following limits:
Let there exist $N \in \N$ such that:
:$\forall n \ge N: x_n \le y_n$
Then:
:$l \le m$
== Proof 1 ==
== Proof 2 ==
== Also known as ==
Category:Inequality Rule for Real Sequences
Category:Limits of Sequences
Category:Real Sequences
Category:Named Theorems
Inequality Rule for Real Sequences/Proof 1

== Theorem == 
== Proof ==
Suppose $l > m$.
Then:
:$m = \dfrac m 2 + \dfrac m 2 < \dfrac {l + m} 2 < \dfrac l 2 + \dfrac l 2 = l$
Let $\epsilon = \dfrac {l - m} 2$.
Then:
:$\epsilon > 0$
We are given that:
:$\ds \lim_{n \mathop \to \infty} x_n = l$
By definition of the limit of a real sequence, we can find $N_1$ such that:
:$\forall n \ge N_1: \size {x_n - l} < \epsilon$
where $\size {x_n - l}$ denotes the absolute value of $x_n - l$
Suppose $n \ge N_1$
If $x_n \ge l$ then $x_n > \dfrac {l + m} 2$
If $x_n < l$ then:
In either case $x_n > \dfrac {l+m} 2$
We are also given that:
:$\ds \lim_{n \mathop \to \infty} y_n = m$
Similarly we can find $N_2$ such that:
:$\forall n > N_2: \size {y_n - m} < \epsilon$
Suppose $n \ge N_2$
If $y_n \le m$ then $y_n < \dfrac {l + m} 2$
If $y_n > m$ then:
In either case $y_n < \dfrac {l + m} 2$
Let $N = \max \set {N_1, N_2}$.
Then if $n > N$, both the above inequalities will be true:
:$n > N_1$
:$n > N_2$
Thus $\forall n > N$:
:$y_n < \dfrac {l + m} 2 < x_n$
It has been shown that:
:$l > m \implies \forall n \in \N: \exists m \ge n: x_n > y_n$
Taking the contrapositive:
:$\exists N \in \N: \forall n \ge N: x_n \le y_n \implies l \le m$
Hence the result.
== Also known as ==
Category:Inequality Rule for Real Sequences
Inequality Rule for Real Sequences/Proof 2

== Theorem == 
== Proof ==
Consider the sequence $\sequence {z_n}$ defined by:
:$z_n := y_n - x_n$
From Sum Rule for Real Sequences:
:$z_n \to m - l$ as $n \to \infty$
Furthermore, the assumption that $x_n \le y_n$ for all $n \in \N$ means that:
:$\forall n \in \N: z_n \ge 0$
Applying the Lower and Upper Bounds for Sequences to the sequence $\sequence {z_n}$ leads to the conclusion that $m - l \ge 0$.
That is:
:$l \le m$
== Also known as ==
Category:Inequality Rule for Real Sequences
Inequality for Ordinal Exponentiation

== Theorem ==
Let $x$ and $y$ be ordinals.
Let $x$ be a limit ordinal and let $y > 0$.
Let $\sequence {a_i}$ be a sequence of ordinals that is strictly decreasing on $1 \le i \le n$.
Let $\sequence {b_i}$ be a sequence of natural numbers.
Then:
:$\ds \paren {\sum_{i \mathop = 1}^n x^{a_i} \times b_i}^y \le x^{a_1 \mathop \times y} \times \paren {b_1 + 1}$
== Proof ==
By Upper Bound of Ordinal Sum:
:$\ds \sum_{i \mathop = 1}^n \paren {x^{a_i} \times b_i} \le x^{a_1} \times \paren {b_1 + 1}$
So:
== Also see ==
* Definition:Cantor Normal Form
== Sources ==
* : $\S 8.48$
Category:Ordinal Arithmetic
Inequality iff Difference is Positive

== Theorem ==
Let $x, y \in \R$.
Then the following are equivalent:
:$(1): \quad x < y$
:$(2): \quad y - x > 0$
== Proof ==
Hence the result.
== Note ==
If the notion of an ordering on $\R$ has not already been defined rigorously, this is often taken to be the definition of $x < y$.
== Sources ==
* : $\S 2.3$: Inequalities
Category:Inequalities
Category:Real Numbers
Inequality of Height of Proper Ideal

== Theorem ==
Let $A$ be a commutative ring with unity.
Let $I$ be a proper ideal in $A$.
Then:
:$\map {\operatorname {dim_{Krull} } } {A / I} + \map {\operatorname {ht} } I \le \map {\operatorname {dim_{Krull} } } A$
where:
:$A/I$ is the quotient ring of $A$ by $I$
:$\operatorname {dim_{Krull} }$ denotes the Krull dimension
:$\map {\operatorname {ht} } I$ is the height of $I$
== Proof ==
Let:
:$n := \map {\operatorname {dim_{Krull} } } {A / I}$
Then there are $\mathfrak q_0, \ldots, \mathfrak q_n \in \Spec {A / I}$ such that:
:$\mathfrak q_0 \subsetneqq \cdots \subsetneqq \mathfrak q_n$
Let $\pi : A \to A / I$ be the quotient epimorphism.
Let:
:$\tilde {\mathfrak q_i} := \pi^{-1} \sqbrk {\mathfrak q_i}$
for $i=0, \ldots, n$.
Then:
:$\tilde {\mathfrak q_0}, \ldots, \tilde {\mathfrak q_n} \in \Spec A$
and:
:$(1):\quad I \subseteqq \tilde {\mathfrak q_0} \subsetneqq \cdots \subsetneqq \tilde {\mathfrak q_n}$
On the other hand, let:
:$m := \map {\operatorname {ht} } {\tilde {\mathfrak q_0} }$
Then there exist $\mathfrak p_0, \ldots, \mathfrak p_m \in \Spec A$ such that:
:$(2):\quad \mathfrak p_0 \subsetneqq \cdots \subsetneqq \mathfrak p_m = \tilde {\mathfrak q_0}$
Hence:
== Sources ==
* $12:$ Dimension
Category:Commutative Algebra
Inequality of Natural Numbers is Provable

== Theorem ==
Let $x, y \in \N$ be natural numbers.
Suppose $x \ne y$.
Let $\sqbrk a$ denote the unary representation of $a \in \N$.
Then $\sqbrk x \ne \sqbrk y$ is a theorem of minimal arithmetic.
== Proof ==
=== Lemma ===
As $x \ne y$, by Ordering on Natural Numbers is Trichotomy, either $x < y$ or $y < x$.
If $y < x$, the result follows from the lemma.
If $x < y$, then:
:$\sqbrk y \ne \sqbrk x$
is a theorem by the lemma.
Hence, the following formal proof:
:By Rule of Assumption, suppose $\sqbrk x = \sqbrk y$
:By Equality is Symmetric, $\sqbrk y = \sqbrk x$
:By Principle of Non-Contradiction, this contradicts $\sqbrk y \ne \sqbrk x$
:By Proof by Contradiction, $\sqbrk x \ne \sqbrk y$
demonstrates the result.
The overall result follows from Proof by Cases.
Category:Inequality of Natural Numbers is Provable
Category:Natural Numbers
Category:Proofs by Induction
Inequality of Natural Numbers is Provable/Lemma

== Lemma for Inequality of Natural Numbers is Provable ==
Let $x, y \in \N$ be natural numbers.
Suppose $x < y$.
Then $\sqbrk y \ne \sqbrk x$ is a theorem of minimal arithmetic.
== Proof ==
Fix $z \in \N_{> 0}$.
Proceed by induction on $x$:
=== Basis for the Induction ===
Suppose $x = 0$.
By Ordering of Natural Numbers is Provable:
:$0 < \sqbrk z$
is a theorem.
The result:
:$\sqbrk z \ne 0$
follows from Axiom $\text M 9$.
=== Induction Hypothesis ===
Suppose that:
:$\sqbrk {x + z} \ne \sqbrk x$
is a theorem.
=== Induction Step ===
The following is a formal proof:
:By the induction hypothesis:
::$\sqbrk {x + z} \ne \sqbrk x$
:By Axiom $\text M 2$:
::$\map s {\sqbrk {x + z} } = \map s {\sqbrk x} \implies \sqbrk {x + z} = \sqbrk x$
:By Rule of Transposition and Modus Ponendo Ponens:
::$\map s {\sqbrk {x + z} } \ne \map s {\sqbrk x}$
But:
:$\map s {\sqbrk {x + z} }$ is identical to $\sqbrk {\map s x + z}$
:$\map s {\sqbrk x}$ is identical to $\sqbrk {\map s x}$
Therefore:
:$\sqbrk {\map s x + z} \ne \sqbrk {\map s x}$
is a theorem.
By Principle of Mathematical Induction:
:$\sqbrk {x + z} \ne \sqbrk x$
is a theorem for every $x \in \N$.
By definition of ordering on natural numbers:
$\exists z \in \N_{> 0}: x + z = y$
By the above:
:$\sqbrk {x + z} \ne \sqbrk x$
is a theorem.
But as $x + z = y$, it is identical to:
:$\sqbrk y \ne \sqbrk x$
Hence the result.
Category:Inequality of Natural Numbers is Provable
Inequality with Meet Operation is Equivalent to Inequality with Relative Pseudocomplement in Brouwerian Lattice

== Theorem ==
Let $\struct {S, \vee, \wedge, \preceq}$ be s Brouwerian lattice.
Let $a, x, y \in S$.
Then
:$a \wedge x \preceq y$ $x \preceq a \to y$
== Proof ==
Define a mapping $d: S \to S$:
:$\forall s \in S: \map d s = a \wedge s$
Define a mapping $g: S \to S$:
:$\forall s \in S: \map g s = a \to s$
By Relative Pseudocomplement and Shift Mapping form Galois Connection in Brouwerian Lattice:
:$\tuple {g, d}$ is Galois connection.
By definition of Galois connection:
:$x \preceq \map g y$ $\map d x \preceq y$
Thus by definitions of $g$ and $d$:
:$a \wedge x \preceq y$ $x \preceq a \to y$
== Sources ==
* 
* 
Category:Brouwerian Lattices
Inertia Principle

== Theorem ==
Let $\sequence {a_n}$ be a sequence in $\R$.
Let $a_n \to l$ as $n \to \infty$.
Let $c \in \R$: such that $c < l$.
Then $\exists N \in \N$ such that:
: $\forall n \in \N: n \ge N \implies c < a_n$
== Proof ==
Pick $\epsilon = l - c > 0$ (as $c < l$).
As $a_n \to l$ as $n \to \infty$, then $\exists N \in \N$ such that:
:$\forall n \in \N: n \ge N \implies \size {a_n - l} < \epsilon$
Equivalently:
:$\forall n \in \N: n \ge N \implies \size {l - a_n} < l - c$
For each $a_n$, either $a_n \ge l$ or $a_n < l$.
If $a_n < l$, then $0 < l - a_n$, so $\size {l - a_n} = l - a_n$.
Then:
If $a_n \ge l$, and $l > c$, then $a_n > c$.
So:
:$\forall n \in \N: n \ge N \implies a_n > c$
== Note ==
Not to be confused with the Principle of Inertia.
Category:Convergence
Category:Sequences
Category:Named Theorems
Infima Inheriting Ordered Subset of Complete Lattice is Complete Lattice

== Theorem ==
Let $L = \struct {X, \preceq}$ be a complete lattice.
Let $S = \struct {T, \precsim}$ be an infima inheriting ordered subset of $L$.
Then $S$ is a complete lattice.
== Proof ==
Let $A$ be subset of $T$.
By definition of complete lattice:
:$A$ admits an infimum in $L$.
Thus by definition of infima inheriting:
:$A$ admits an infimum in $S$.
Hence by dual of Lattice is Complete iff it Admits All Suprema:
:$S$ is a complete lattice.
== Sources ==
* 
Category:Complete Lattices