nyuuzyou/wikis huggingface dataset:
Weierstrass Function is Continuous

== Theorem ==
Let $a \in \openint 0 1$. 
Let $b$ be a strictly positive odd integer such that: 
:$\ds a b > 1 + \frac 3 2 \pi$
Let $f: \R \to \R$ be a real function defined by: 
:$\ds \map f x = \sum_{n \mathop = 0}^\infty a^n \map \cos {b^n \pi x}$
for each $x \in \R$.
Then $f$ is well-defined and continuous.
== Proof ==
Note that: 
:$\ds \sup_{x \mathop \in \R} \size {a^n \map \cos {b^n \pi x} } = a^n$
Since $a \in \openint 0 1$:
:$\ds \sum_{n \mathop = 0}^\infty a^n$ converges.
So, by the Weierstrass M-Test:
:$\ds \sum_{n \mathop = 0}^\infty a^n \map \cos {b^n \pi x}$ converges uniformly on $\R$. 
That is, $f$ is well-defined.
Further, from Uniformly Convergent Series of Continuous Functions Converges to Continuous Function: Corollary:
:$f$ is continuous.
Category:Weierstrass Function
Weierstrass M-Test

== Theorem ==
Let $f_n$ be a sequence of real functions defined on a domain $D \subseteq \R$.
Let $\ds \sup_{x \mathop \in D} \size {\map {f_n} x} \le M_n$ for each integer $n$ and some constants $M_n$
Let $\ds \sum_{i \mathop = 1}^\infty M_i < \infty$.
Then $\ds \sum_{i \mathop = 1}^\infty f_i$ converges uniformly on $D$.
== Proof ==
Let:
:$\ds S_n = \sum_{i \mathop = 1}^n f_i$
Let:
:$\ds f = \lim_{n \mathop \to \infty} S_n$
To show the sequence of partial sums converge uniformly to $f$, we must show that:
:$\ds \lim_{n \mathop \to \infty} \sup_{x \mathop \in D} \size {f - S_n} = 0$
But:
By the Triangle Inequality, this value is less than or equal to:
:$\ds \sum_{i \mathop = n + 1}^\infty \sup_{x \mathop \in D} \size {\map {f_i} x} \le \sum_{i \mathop = n + 1}^\infty M_i$
We have that:
:$\ds 0 \le \sum_{i \mathop = 1}^\infty M_n < \infty$
It follows from Tail of Convergent Series tends to Zero:
:$\ds 0 \le \lim_{n \mathop \to \infty} \sum_{i \mathop = n + 1}^\infty \sup_{x \mathop \in D} \size {\map {f_i} x} \le \lim_{n \mathop \to \infty} \sum_{i \mathop = n + 1}^\infty M_i = 0$
So:
:$\ds \lim_{n \mathop \to \infty} \sup_{x \mathop \in D} \size {f - S_n} = 0$
Hence the series converges uniformly on the domain.
== Also known as ==
Some sources do not use the hyphen: Weierstrass $M$ test.
== Historical Note ==
== Sources ==
* : $\S 9.6$: Uniform Convergence of Infinite Series of Functions: Theorem $9.6$
* : $\S 1.3$: Infinite series of functions: Theorem $1.8$
Category:Real Analysis
Category:Convergence
Weierstrass Product Inequality

== Theorem ==
For $n \ge 1$:
:$\ds \prod_{i \mathop = 1}^n \paren {1 - a_i} \ge 1 - \sum_{i \mathop = 1}^n a_i$
where all of $a_i$ are in the closed interval $\closedint 0 1$.
== Proof ==
For $n = 1$ we have:
:$1 - a_1 \ge 1 - a_1$
which is clearly true. 
Suppose the proposition is true for $n = k$, that is:
:$\ds \prod_{i \mathop = 1}^k \paren {1 - a_i} \ge 1 - \sum_{i \mathop = 1}^k a_i$
Then:
Thus, by Principle of Mathematical Induction, the proof is complete. 
== Also see ==
* Bounds for Finite Product of Real Numbers
== Sources ==
* 
Category:Inequalities
Category:Infinite Products
Weierstrass Product Theorem

== Theorem ==
Let $\sequence {a_k}$ be a sequence of non-zero complex numbers such that:
:$\cmod {a_n} \to \infty$ as $n \to \infty$
Let $\sequence {p_n}$ be a sequence of non-negative integers for which the series:
:$\ds \sum_{n \mathop = 1}^\infty \size {\dfrac r {a_n} }^{1 + p_n}$
converges for every $r \in \R_{> 0}$.
Let:
:$\ds \map f z = \prod_{n \mathop = 1}^\infty \map {E_{p_n} } {\frac z {a_n} }$
where $E_{p_n}$ are Weierstrass elementary factors.
Then $f$ is entire and its zeroes are the points $a_n$, counted with multiplicity.
== Proof ==
By:
:Locally Uniformly Absolutely Convergent Product is Locally Uniformly Convergent
:Infinite Product of Analytic Functions is Analytic
:Zeroes of Infinite Product of Analytic Functions
it suffices to show that the product $\ds \prod_{n \mathop = 1}^\infty \map {E_{p_n} } {\frac z {a_n} }$ converges locally uniformly absolutely.
By Bounds for Weierstrass Elementary Factors and Weierstrass M-Test, this is the case.
== Also see ==
* Weierstrass Factorization Theorem
Category:Infinite Products
Weierstrass Substitution

== Proof Technique ==
The Weierstrass substitution is an application of Integration by Substitution.
The substitution is:
:$u \leftrightarrow \tan \dfrac \theta 2$
for $-\pi < \theta < \pi$, $u \in \R$.
It yields:
=== Sine ===
=== Cosine ===
=== Derivative ===
The above results can be stated:
:$\ds \int \map F {\sin \theta, \cos \theta} \rd \theta = 2 \int \map F {\frac {2 u} {1 + u^2}, \frac {1 - u^2} {1 + u^2} } \frac {d u} {1 + u^2}$
where $u = \tan \dfrac \theta 2$.
== Also known as ==
== Also see ==
* Hyperbolic Tangent Half-Angle Substitution
== Sources ==
* : $\text {II}$. Calculus: Integration: Useful substitutions: Example $1$.
* : $\S 14$: Indefinite Integrals: Important Transformations: $14.58$
* 
* 
* : $\S 16$: Indefinite Integrals: Important Transformations: $16.58.$
* 
* 
Category:Weierstrass Substitution
Category:Integral Substitutions
Category:Primitives involving Sine Function
Category:Primitives involving Cosine Function
Category:Proof Techniques
Weierstrass Substitution/Also known as

== Weierstrass Substitution: Also known as ==
The technique of Weierstrass Substitution is also known as Tangent Half-Angle Substitution.
Some sources call these results the Tangent-of-Half-Angle Formulae.
Other sources refer to them merely as the Half-Angle Formulas or Half-Angle Formulae.
== Sources ==
* 
* 
* : Appendix $12$: Trigonometric formulae: Tangent-of-half-angle formulae
* : Appendix $14$: Trigonometric formulae: Tangent-of-half-angle formulae
Category:Weierstrass Substitution
Weierstrass Substitution/Cosine

== Proof Technique ==
Let:
:$u \leftrightarrow \tan \dfrac \theta 2$
for $-\pi < \theta < \pi$, $u \in \R$.
Then:
:$\cos \theta = \dfrac {1 - u^2} {1 + u^2}$
== Proof ==
Let $u = \tan \dfrac \theta 2$ for $-\pi < \theta < \pi$.
From Shape of Tangent Function, this substitution is valid for all real $u$.
Then:
== Also known as ==
== Also see ==
* Hyperbolic Tangent Half-Angle Substitution
== Sources ==
* : $\text {II}$. Calculus: Integration: Useful substitutions: Example $1$.
* 
* 
* 
* 
* : Appendix $12$: Trigonometric formulae: Tangent-of-half-angle formulae
* : Appendix $14$: Trigonometric formulae: Tangent-of-half-angle formulae
* 
Category:Weierstrass Substitution
Weierstrass Substitution/Derivative

== Proof Technique ==
Let:
:$u \leftrightarrow \tan \dfrac \theta 2$
for $-\pi < \theta < \pi$, $u \in \R$.
Then:
:$\dfrac {\d \theta} {\d u} = \dfrac 2 {1 + u^2}$
== Proof ==
Let $u = \tan \dfrac \theta 2$ for $-\pi < \theta < \pi$.
From Shape of Tangent Function, this substitution is valid for all real $u$.
Then:
== Also known as ==
== Also see ==
* Hyperbolic Tangent Half-Angle Substitution
== Sources ==
* : $\text {II}$. Calculus: Integration: Useful substitutions: Example $1$.
* 
Category:Weierstrass Substitution
Weierstrass Substitution/Sine

== Proof Technique ==
Let:
:$u \leftrightarrow \tan \dfrac \theta 2$
for $-\pi < \theta < \pi$, $u \in \R$.
Then:
:$\sin \theta = \dfrac {2 u} {1 + u^2}$
== Proof ==
Let $u = \tan \dfrac \theta 2$ for $-\pi < \theta < \pi$.
From Shape of Tangent Function, this substitution is valid for all real $u$.
Then:
== Also known as ==
== Also see ==
* Hyperbolic Tangent Half-Angle Substitution
== Sources ==
* : $\text {II}$. Calculus: Integration: Useful substitutions: Example $1$.
* 
* 
* 
* 
* : Appendix $12$: Trigonometric formulae: Tangent-of-half-angle formulae
* : Appendix $14$: Trigonometric formulae: Tangent-of-half-angle formulae
* 
Category:Weierstrass Substitution
Weight of Body at Earth's Surface

== Theorem ==
Let $B$ be a body of mass $m$ situated at (or near) the surface of Earth.
Then the weight of $B$ is given by:
:$W = m g$
where $g$ is the value of the acceleration due to gravity at the surface of Earth.
== Proof ==
The weight of $B$ is the magnitude of the force exerted on it by the influence of the gravitational field it is in.
By Newton's Second Law of Motion, that force is given by:
:$\mathbf W = -m g \mathbf k$
where:
:$g$ is the value of the acceleration due to gravity at the surface of Earth
:$\mathbf k$ is a unit vector directed vertically upwards.
Hence the magnitude of $\mathbf W$ is given by:
:$W = \size {-m g \mathbf k} = m g$
== Sources ==
* 
* 
Category:Weight (Physics)
Weight of Discrete Topology equals Cardinality of Space

== Theorem ==
Let $T = \struct {S, \tau}$ be a discrete topological space.
Then:
:$\map w T = \size S$
where:
:$\map w T$ denotes the weight of $T$
:$\card S$ denotes the cardinality of $S$.
== Proof ==
By Basis for Discrete Topology the set $\BB = \set {\set x: x \in S}$ is a basis of $T$.
By Set of Singletons is Smallest Basis of Discrete Space $\BB$ is smallest basis of $T$:
:for every basis $\CC$ of $T$, $\BB \subseteq \CC$.
Then by Subset implies Cardinal Inequality:
:for every basis $\CC$ of $T$, $\card \BB \le \card \CC$.
Hence $\card \BB$ is minimal cardinalty of basis of $T$:
:$\map w T = \card \BB$ by definition of weight.
Thus by Cardinality of Set of Singletons:
:$\map w T = \card S$
== Sources ==
* 
* 
Category:Discrete Topology
Weight of Linear Codeword/Examples/Codeword in V(4,3)

== Example of Weight of Linear Codeword ==
In the master code $\map V {4, 3}$, the codeword $1201$ has a weight of $3$.
== Proof ==
This is because it has $3$ non-zero digits.
== Sources ==
* : Chapter $6$: Error-correcting codes: Example $6.6$
Category:Examples of Linear Codes
Weight of Sorgenfrey Line is Continuum

== Theorem ==
Let $T = \struct {\R, \tau}$ be the Sorgenfrey line.
Then $\map w T = \mathfrak c$
where
:$\map w T$ denotes the weight of $T$
:$\mathfrak c$ denotes continuum, the cardinality of real numbers.
== Proof ==
By definition of Sorgenfrey line, the set:
:$\BB = \set {\hointr x y: x, y \in \R \land x < y}$
is a basis of $T$.
By definition of weight:
:$\map w T \le \card \BB$
where $\card \BB$ denotes the cardinality of $\BB$.
By Cardinality of Basis of Sorgenfrey Line not greater than Continuum:
:$\card \BB \le \mathfrak c$
Thus
:$\map w T \le \mathfrak c$
It remains to show that:
:$\mathfrak c \le \map w T$
:$\mathfrak c \not \le \map w T$
Then:
:$\map w T < \mathfrak c$
By definition of weight, there exists a basis $\BB_0$ of $T$:
:$\map w T = \card {\BB_0}$
Then by Set of Subset of Reals with Cardinality less than Continuum has not Interval in Union Closure:
:$\exists x, y \in \R: x < y \land \hointr x y \notin \set {\bigcup A: A \subseteq \BB_0} = \tau$
By definition of $\BB$:
:$\hointr x y \in \BB \subseteq \tau$
Thus this contradicts by definition of subset with:
:$\hointr x y \notin \tau$
== Sources ==
* 
* 
Category:Sorgenfrey Line
Weird Number/Examples/4030

== Example of a Weird Number ==
$4030$ is a weird number:
The aliquot sum of $4030$ is $4034$, but no subset of its aliquot parts add to $4030$.
== Proof ==
From :
:$\map {\sigma_1} {4030} = 8064$
where $\map {\sigma_1} {4030}$ denotes the divisor sum function.
The aliquot sum of $4030$ is given by:
:$\map {\sigma_1} {4030} - 4030 = 8064 - 4030 = 4034$
The aliquot parts of $4030$ are found in :
:$1, 2, 5, 10, 13, 26, 31, 62, 65, 130, 155, 310, 403, 806, 2015$
Note that $4$ is not an aliquot part of $4030$, and cannot be made from the aliquot parts of $4030$.
Thus $4030 = 4034 - 4$ cannot be made by any combination of those aliquot parts.
Hence the result.
Category:Weird Numbers
Category:4030
Weird Number/Examples/70

== Example of a Weird Number ==
$70$ is a weird number:
The aliquot sum of $70$ is $74$, but no subset of its aliquot parts add to $70$.
== Proof ==
From :
:$\map {\sigma_1} {70} = 144$
where $\sigma_1$ denotes the divisor sum.
The aliquot sum of $70$ is given by:
:$\map {\sigma_1} {70} - 70 = 144 - 70 = 74$
The aliquot parts of $70$ are:
:$1, 2, 5, 7, 10, 14, 35$
Note that $4$ is not an aliquot part of $70$.
Thus $70 = 74 - 4$ cannot be made by any combination of those aliquot parts.
Hence the result.
== Sources ==
* : $70$
* : $70$
Category:Weird Numbers
Category:70
Weird Number/Examples/836

== Example of a Weird Number ==
$836$ is a weird number:
The aliquot sum of $836$ is $844$, but no subset of its aliquot parts add to $836$.
== Proof ==
From :
:$\map {\sigma_1} {836} = 1680$
where $\sigma_1$ denotes the divisor sum function.
The aliquot sum of $836$ is given by:
:$\map {\sigma_1} {836} - 836 = 1680 - 836 = 844$
The aliquot parts of $836$ are found in :
:$1, 2, 4, 11, 19, 22, 38, 44, 76, 209, 418$
Note that $8$ is not an aliquot part of $836$, and cannot be made from the aliquot parts of $836$.
Thus $836 = 844 - 8$ cannot be made by any combination of those aliquot parts.
Hence the result.
Category:Weird Numbers
Category:836
Well-Defined Jordan Content Equals Content

== Theorem ==
Let $M$ be a bounded subspace of Euclidean space.
Let the Jordan content of $M$ be $\map m M$.
Then the content $\map V M = \map m M$.
== Proof ==
Let $C$ be a finite covering of $M$.
By , $\map V C \ge \map V M$.
Therefore, $\map V M$ is a lower bound of all $\map V C$.
So by the definition of greatest lower bound:
:$\map V M \le \map {m^*} M$
Let $D$ be a finite covering of $S \setminus M$.
By the same reasoning:
:$\map V {S \setminus M} \le \map {m^*} {S \setminus M}$
But:
Therefore:
:$\map V S - \map {m^*} {S \setminus M} \le \map V M \le \map {m^*} M$
But by hypothesis:
:$\map V S - \map {m^*} {S \setminus M} = \map {m^*} M = \map m M$
So it follows that:
:$\map V M = \map m M$
Well-Defined Mapping/Examples/Floor of Half Function on Congruence Modulo 6

== Example of Mapping which is not Well-Defined ==
Let $x \mathrel {C_6} y$ be the equivalence relation defined on the natural numbers as congruence modulo $6$:
:$x \mathrel {C_6} y \iff x \equiv y \pmod 6$
defined as:
:$\forall x, y \in \N: x \equiv y \pmod 6 \iff \exists k, l, m \in \N, m < 6: 6 k + m = x \text { and } 6 l + m = y$
Let $\eqclass x {C_6}$ denote the equivalence class of $x$ under $C_6$.
Let $\N / {C_6}$ denote the quotient set of $\N$ by $C_6$.
Let us define the mapping $\phi$ on $\N / {C_6}$ as follows:
:$\map \phi {\eqclass x {C_6} } = \eqclass {\floor {x / 2} } {C_6}$
where $\floor {\, \cdot \,}$ denotes the floor function.
Then $\phi$ is not a well-defined mapping.
== Proof ==
Consider $x = 4$ and $x' = 10$.
We have that:
:$4 = 6 \times 0 + 4$
and:
:$10 = 6 \times 1 + 4$
and so:
:$4 \mathrel {C_6} {10}$
That is:
:$\eqclass 4 {C_6} = \eqclass {10} {C_6}$
However, we have that:
:$\map \phi {\eqclass 4 {C_6} } = \eqclass 2 {C_6}$
while:
:$\map \phi {\eqclass {10} {C_6} } = \eqclass 5 {C_6}$
But $\eqclass 2 {C_6} \ne \eqclass 5 {C_6}$
Hence we have $x, x' \in \N$ for which it is not the case that:
:$\map \phi {\eqclass x {C_6} } = \map \phi {\eqclass {x'} {C_6} }$
That is, $\phi$ is not well-defined.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $1$: Pairs, Relations, and Functions
Category:Examples of Well-Defined Mappings‎
Well-Defined Mapping/Examples/Square Function on Congruence Modulo 6

== Example of Well-Defined Mapping ==
Let $x \mathrel {C_6} y$ be the equivalence relation defined on the natural numbers as congruence modulo $6$:
:$x \mathrel {C_6} y \iff x \equiv y \pmod 6$
defined as:
:$\forall x, y \in \N: x \equiv y \pmod 6 \iff \exists k, l, m \in \N, m < 6: 6 k + m = x \text { and } 6 l + m = y$
Let $\eqclass x {C_6}$ denote the equivalence class of $x$ under $C_6$.
Let $\N / {C_6}$ denote the quotient set of $\N$ by $C_6$.
Let us define the mapping $\mathrm {sq}$ on $\N / {C_6}$ as follows:
:$\map {\mathrm {sq} } {\eqclass x {C_6} } = m^2$
where $x = 6 k + m$ for some $k, m \in \N$ such that $m < 6$.
Then $\mathrm {sq}$ is a well-defined mapping.
== Proof ==
Let:
:$x \mathrel {C_6} x'$
for arbitrary $x, x' \in \N$.
We need to demonstrate that:
:$\map {\mathrm {sq} } {\eqclass x {C_6} } = \map {\mathrm {sq} } {\eqclass {x'} {C_6} }$
Let $m, n \in \N$ such that:
:$\map {\mathrm {sq} } {\eqclass x {C_6} } = m^2$
:$\map {\mathrm {sq} } {\eqclass {x'} {C_6} } = n^2$
We have by definition of $C_6$ that:
:$x \mathrel {C_6} x' \iff \exists k, l, m \in \N, m < 6: 6 k + m = x \text { and } 6 l + m = x'$
Hence:
:$\map {\mathrm {sq} } {\eqclass {x'} {C_6} } = m^2$
But for $m^2 \ne n^2$ where $0 \le m < 6$ and $0 \le n < 6$:
:$m = n$
and the result follows.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $1$: Pairs, Relations, and Functions: Exercise $11 \ \text {(b)}$
Category:Examples of Well-Defined Mappings‎
Well-Defined Mapping/Motivation

== Motivation for Well-Defined Mapping ==
Suppose we are given a mapping $f: S \to T$.
Suppose we have an equivalence $\RR$ on $S$, and we want to define a mapping on the quotient set:
:$\phi: S / \RR \to T$
such that:
:$\map \phi {\eqclass \cdots \RR} = \map f \cdots$
That is, we want every element of a given equivalence class to map to the same element of the codomain of $f$.
The only way this can be done is to set $\map \phi {\eqclass x \RR} = \map f x$.
Now, if $x, y \in S$ are in the same equivalence class class with respect to $\RR$, that is, in order for $\map \phi {\eqclass x \RR}$ to make any sort of sense, we need to make sure that $\map \phi {\eqclass x \RR} = \map \phi {\eqclass y \RR}$, or (which comes to the same thing) $\map f x = \map f y$.
So $\map \phi {\eqclass x \RR} = \map f x$ defines a mapping $\phi: S / \RR \to T$ $\forall \tuple {x, y} \in \RR: \map f x = \map f y$.
If this holds, then the mapping $\phi$ is well-defined.
The terminology is misleading, as $\phi$ cannot be defined at all if the condition is not met.
What this means is: if we want to define a mapping from a quotient set to any other set, then all the individual elements of each equivalence class in the domain must map to the same element in the codomain.
Therefore, when attempting to construct or analyse such a mapping, it is necessary to check for well-definedness.
== Sources ==
* : Chapter $1$: Equivalence Relations: $\S 19$
* : Part $1$: Not Entirely Naive Set Theory: Chapter $1$: Pairs, Relations, and Functions
Category:Well-Defined Mappings
Category:Quotient Sets
Well-Defined Relation/Examples/Less Than on Congruence Modulo 6

== Example of Well-Defined Relation ==
Let $x \mathrel {C_6} y$ be the equivalence relation defined on the natural numbers as congruence modulo $6$:
:$x \mathrel {C_6} y \iff x \equiv y \pmod 6$
defined as:
:$\forall x, y \in \N: x \equiv y \pmod 6 \iff \exists k, l, m \in \N, m < 6: 6 k + m = x \text { and } 6 l + m = y$
Let $\eqclass x {C_6}$ denote the equivalence class of $x$ under $C_6$.
Let $\N / {C_6}$ denote the quotient set of $\N$ by $C_6$.
Let us define the relation $L$ on $\N / {C_6}$ as follows:
:$\tuple {\eqclass x {C_6}, \eqclass y {C_6} } \in L \iff \exists k, l, m, n \in \N, m < n < 6: x = 6 k + m, y = 6 l + n$
Then $L$ is a well-defined relation.
== Proof ==
Let:
:$x \mathrel {C_6} x'$
:$y \mathrel {C_6} y'$
for arbitrary $x, y, x', y' \in \N$.
We need to demonstrate that:
:$\tuple {\eqclass x {C_6}, \eqclass y {C_6} } \in L \iff \tuple {\eqclass {x'} {C_6}, \eqclass {y'} {C_6} } \in L$
So:
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $1$: Pairs, Relations, and Functions: Exercise $11 \ \text {(a)}$
Category:Well-Defined Relations
Well-Founded Induction

== Theorem ==
Let $\struct {A, \RR}$ be a strictly well-founded relation.
Let $\RR^{-1} \sqbrk x$ denote the preimage of $x$ for each $x \in A$.
Let $B$ be a class such that $B \subseteq A$.
Suppose that:
:$(1): \quad \forall x \in A: \paren {\RR^{-1} \sqbrk x \subseteq B \implies x \in B}$
Then:
:$A = B$
That is, if a property passes from the preimage of $x$ to $x$, then this property is true for all $x \in A$.
== Proof ==
 $A \nsubseteq B$.
Then:
:$A \setminus B \ne 0$
By Strictly Well-Founded Relation determines Strictly Minimal Elements, $A \setminus B$ must have some strictly minimal element under $\RR$.
Let $\map \complement B$ be the set complement of $B$.
Then:
So, by Intersection with Complement is Empty iff Subset:
:$A \cap \RR^{-1} \sqbrk x \subseteq B$
Since $\RR^{-1} \sqbrk x \subseteq A$, by definition of a subset:
:$\RR^{-1} \sqbrk x \subseteq B$
Thus, $(1)$:
:$x \in B$
But this contradicts the fact that:
:$x \in A \setminus B$
By Proof by Contradiction it follows that:
:$A \setminus B = \O$
and so:
:$A \subseteq B$
Therefore:
:$A = B$
== Also see ==
Well-Ordered Induction, a weaker theorem that does not require the Axiom of Foundation.
== Sources ==
* : $\S 9.22$
Category:Axiom of Foundation
Category:Set Theory
Well-Founded Proper Relational Structure Determines Minimal Elements

== Theorem ==
Let $A$ and $B$ be classes.
Let $\struct {A, \prec}$ be a proper relational structure.
Let $\prec$ be a strictly well-founded relation.
Suppose $B \subset A$ and $B \ne \O$.
Then $B$ has a strictly minimal element under $\prec$.
== Proof ==
$B$ is not empty.
So $B$ has at least one element $x$.
By Singleton of Element is Subset:
:$\set x \subseteq B$
By Relational Closure Exists for Set-Like Relation:
:$\set x$ has a $\prec$-relational closure.
This $\prec$-relational closure shall be denoted $y$.
By Intersection is Subset:
:$y \cap B \subseteq A$
As $x \in y$ and $x \in B$:
:$y \cap B \ne \O$
By the definition of strictly well-founded relation:
:$(1): \quad \exists x \in \paren {y \cap B}: \forall w \in \paren {y \cap B}: w \nprec x$
 that $w \in B$ such that $w \prec x$.
Since $x \in y$, it follows that $w \in y$, so $w \in \paren {B \cap y}$ by the definition of intersection.
This contradicts $(1)$.
Therefore:
:$w \nprec x$
and so $B$ has a strictly minimal element under $\prec$.
== Sources ==
* : $\S 9.4$
Category:Relational Closures
Well-Founded Recursion

== Theorem ==
Let $A$ be a class.
Let $\RR$ be a relation that is strictly well-founded on $A$.
Let every $\RR$-initial segment of any element $x$ of $A$ be a small class.
Let $G$ be a (class) mapping from $A^A$ to $A$.
Let $K$ be a class of mappings $f$ that satisfy:
:$(1): \quad$ The domain of $f$ is some subset $y \subseteq A$ such that $y$ is transitive with respect to $\RR$.
:$(2): \quad \forall x \in y: \map f x = \map G {f \restriction \RR^{-1} x}$
where $f \restriction R^{-1} x$ denotes the restriction of $f$ to the $\RR$-initial segment of $x$.
Let $F = \bigcup K$, the union of $K$.
Then:
:$F$ is a mapping with domain $A$
:$\forall x \in A: \map F x = \map G {F \restriction \RR^{-1} x}$
:$F$ is unique, in the sense that if another mapping $A$ has the above two properties, then $A = F$.
== Proof ==
== Sources ==
* : $\S 9.7$
Category:Relational Closures
Well-Founded Relation has no Relational Loops

== Theorem ==
Let $\RR$ be a well-founded relation on $S$.
Let $x_1, x_2, \ldots, x_n \in S$.
Then:
:$\neg \paren {\paren {x_1 \mathrel \RR x_2} \land \paren {x_3 \mathrel \RR x_4} \land \cdots \land \paren {x_n \mathrel \RR x_1} }$
That is, there are no relational loops within $S$.
== Proof ==
Since $x_1, x_2, \ldots, x_n \in S$, there exists a non-empty subset $T$ of $S$ such that:
:$T = \set {x_1, x_2, \ldots, x_n}$
By the definition of a well-founded relation:
:$(1): \quad \exists z \in T: \forall y \in T \setminus z: \neg y \mathrel \RR z$
 $\paren {x_1 \mathrel \RR x_2} \land \paren {x_2 \mathrel \RR x_3} \land \cdots \land \paren {x_n \mathrel \RR x_1}$.
We have that the elements of $T$ are $x_1, x_2, \ldots, x_n$.
Hence:
:$\forall y \in T: \exists z \in T \setminus z: y \mathrel \RR z$
This then contradicts $(1)$.
Hence:
:$\neg \paren {\paren {x_1 \mathrel \RR x_2} \land \paren {x_3 \mathrel \RR x_4} \land \cdots \land \paren {x_n \mathrel \RR x_1} }$
and so it follows that a well-founded relation has no relational loops.
== Sources ==
* : Part $1$: Not Entirely Naive Set Theory: Chapter $2$: Partial Order Relations: Exercise $8$
Category:Well-Founded Relations