avewright/proofwiki-math huggingface dataset:
Theorem: Kernel of Magma Homomorphism is Submagma

Let $\struct {S, *}$ be a magma.
Let $\struct {T, \circ}$ be an algebraic structure with an identity $e$.
Let $\phi: S \to T$ be a homomorphism.
Then the kernel of $\phi$ is a submagma of $\struct {S, *}$.
That is:
:$\struct {\map {\phi^{-1} } e, *}$ is a submagma of $\struct {S, *}$
where $\map {\phi^{-1} } e$ denote the preimage of $e$.

Proof:
Let $x, y \in \map {\phi^{-1} } e$.
By the definition of a magma, $S$ is closed under $*$.
That is:
:$\forall x, y \in S: x * y \in S$
Hence:
:$x * y \in \Dom \phi$
It is to be shown that:
:$x * y \in \map {\phi^{-1} } e$
Thus:
{{begin-eqn}}
{{eqn | l = x, y
      | o = \in
      | r = \map {\phi^{-1} } e
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \phi x
      | r = e
      | c = {{Defof|Kernel of Magma Homomorphism}}
}}
{{eqn | lo= \land
      | l = \map \phi y
      | r = e
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \phi x \circ \map \phi y
      | r = e
      | c = {{Defof|Identity Element}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \map \phi {x * y}
      | r = e
      | c = {{Defof|Homomorphism (Abstract Algebra)}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x*y
      | o = \in
      | r = \map {\phi^{-1} } e
      | c = {{Defof|Preimage of Element under Mapping}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Abstract Algebra
i9vs1hl0ngw6kwo5jg5okrosnrsvcv5
Theorem: Preimage of Zero of Homomorphism is Submagma

Let $\struct {S, *}$ be a magma.
Let $\struct {T, \circ}$ be a magma with a zero element $0$.
Let $\phi: S \to T$ be a magma homomorphism.
Then $\struct {\phi^{-1} \sqbrk 0, *}$ is a submagma of $\struct {S, *}$.

Proof:
Let $x, y \in \phi^{-1} \sqbrk 0$.
It is to be shown that:
:$x * y \in \phi^{-1} \sqbrk 0$
Thus:
{{begin-eqn}}
{{eqn | l = x, y \in \phi^{-1} \sqbrk 0
      | o = \leadstoandfrom
      | r = \paren {\map \phi x = 0} \land \paren {\map \phi y = 0}
      | c = {{Defof|Preimage of Element under Mapping}}
}}
{{eqn | o = \leadstoandfrom
      | r = \map \phi x \circ \map \phi y = 0
      | c = {{Defof|Zero Element}}
}}
{{eqn | o = \leadstoandfrom
      | r = \map \phi {x * y} = 0
      | c = {{Defof|Homomorphism (Abstract Algebra)}}
}}
{{eqn | o = \leadstoandfrom
      | r = x * y \in \phi^{-1} \sqbrk 0
      | c = {{Defof|Preimage of Element under Mapping}}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Abstract Algebra
6xlhe0vgz3184l91icqbi52xt92i8m8
Theorem: Polynomial over Field is Reducible iff Scalar Multiple is Reducible

Let $K$ be a field.
Let $K \sqbrk X$ be the ring of polynomial forms over $K$.
Let $P \in K \sqbrk X$.
Let $\lambda \in K \setminus \set 0$.
Then $P$ is irreducible in $K \sqbrk X$ {{iff}} $\lambda P$ is also irreducible in $K \sqbrk X$.
{{expand|Investigate whether this result also holds where $K$ is a general ring.}}

Proof:
=== Necessary Condition ===
Let $P$ be irreducible.
Suppose further that $ \lambda P$ has a non-trivial factorization:
:$\lambda P = Q_1 Q_2$
that is, such that $Q_1$ and $Q_2$ are not units of $K \sqbrk X$.
By Units of Ring of Polynomial Forms over Field it follows that $\deg Q_1 \ge 1$ and $\deg Q_2 \ge 1$.
Let $Q_1' = \lambda^{-1} Q_1$.
This implies that:
:$P = Q_1' Q_2$
with $\deg Q_1' = \deg Q_1 \ge 1$.
But this is a non-trivial factorization of $P$ in $K \sqbrk X$.
This contradicts our supposition that $P$ is irreducible.
Therefore $\lambda P$ has no non-trivial factorization, that is, $\lambda P$ is irreducible.
{{qed|lemma}}
Theorem: Conjunction of Disjunctions Consequence

:$\paren {p \lor q} \land \paren {r \lor s} \vdash p \lor r \lor \paren {q \land s}$

Proof:
{{BeginTableau|\paren {p \lor q} \land \paren {r \lor s} \vdash \paren {p \lor r} \lor \paren {q \land s} }}
{{Premise|1|\paren {p \lor q} \land \paren {r \lor s} }}
{{SequentIntro|2|1|\paren {p \land \paren {r \lor s} } \lor \paren {q \land \paren {r \lor s} }|1|Conjunction Distributes over Disjunction}}
{{TheoremIntro|3|p \land \paren {r \lor s} \implies p|Simplification}}
{{TheoremIntro|4|q \land \paren {r \lor s} \implies \paren {q \land r} \lor \paren {q \land s}|Conjunction Distributes over Disjunction}}
{{TheoremIntro|5|q \land r \implies r|Simplification}}
{{TheoremIntro|6|q \land s \implies q \land s|Law of Identity/Formulation 2}}
{{SequentIntro|7||\paren {q \land r} \lor \paren {q \land s} \implies r \lor \paren {q \land s}|5,6|Constructive Dilemma}}
{{SequentIntro|8||q \land \paren {r \lor s} \implies r \lor \paren {q \land s}|4,7|Hypothetical Syllogism}}
{{SequentIntro|9||\paren {p \lor q} \land \paren {r \lor s} \implies p \lor \paren {r \lor \paren {q \land s} }|3,8|Constructive Dilemma}}
{{ModusPonens|10|1|p \lor \paren {r \lor \paren {q \land s} }|9|1}}
{{SequentIntro|11|1|\paren {p \lor r} \lor \paren {q \land s}|10|Rule of Association}}
{{EndTableau}}
{{qed}}
Category:Conjunction
Category:Disjunction
7qlx2ukbv57rxya4oqdrqvg0qv5dsve
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 2/Forward Implication

:$\vdash \paren {p \land \paren {q \lor r} } \implies \paren {\paren {p \land q} \lor \paren {p \land r} }$

Proof:
{{BeginTableau|\vdash \paren {p \land \paren {q \lor r} } \implies \paren {\paren {p \land q} \lor \paren {p \land r} } }}
{{Assumption|1|p \land \paren {q \lor r} }}
{{SequentIntro|2|1|\paren {\paren {p \land q} \lor \paren {p \land r} }|1|Conjunction is Left Distributive over Disjunction: Formulation 1}}
{{Implication|3||\paren {p \land \paren {q \lor r} } \implies \paren {\paren {p \land q} \lor \paren {p \land r} }|1|2}}
{{EndTableau}}
{{qed}}
Category:Rule of Distribution
e3qjizjj2x1iup4852sqbocw0rdss1a
Theorem: Existence of Ring of Polynomial Forms in Transcendental over Integral Domain

Let $\struct {R, +, \circ}$ be a commutative ring with unity.
Let $\struct {D, +, \circ}$ be an integral subdomain of $R$ whose zero is $0_D$.
Let $X \in R$ be transcendental over $D$
Then the ring of polynomials $D \sqbrk X$ in $X$ over $D$ exists.

Proof:
{{finish|The following is an outline only}}
Suppose that $D \sqbrk X$ exists.
Let $\ds \map P X = \sum_{k \mathop = 0}^n a_k X^k$, where $a_n \ne 0_D$, be an arbitrary element of $D \sqbrk X$.
Then $\map P X$ corresponds to, and is completely described by, the ordered tuple of coefficients $\tuple {a_0, a_1, \dotsc, a_n, 0_D, 0_D, 0_D, \dotsc}$.
Consider the set $S$ of infinite sequences of elements of $D$ which are eventually $0_D$.
That is, whose elements are of the form $\tuple {b_0, b_1, \dotsc, b_n, 0_D, 0_D, 0_D, \dotsc}$ where $b_0, \ldots, b_n \in D$.
Consider the polynomial ring over $S$ by defining the operations:
{{begin-axiom}}
{{axiom | n = 1
        | lc= '''Ring Addition:'''
        | ml= \sequence {r_0, r_1, r_2, \ldots} + \sequence {s_0, s_1, s_2, \ldots}
        | mo= =
        | mr= \sequence {r_0 + s_0, r_1 + s_1, r_2 + s_2, \ldots}
        | c = 
}}
{{axiom | n = 2
        | lc= '''Ring Negative:'''
        | ml= -\sequence {r_0, r_1, r_2, \ldots}
        | mo= =
        | mr= \sequence {-r_0, -r_1, -r_2, \ldots}
        | c = 
}}
{{axiom | n = 3
        | lc= '''Ring Product:'''
        | ml= \sequence {r_0, r_1, r_2, \ldots} \circ \sequence {s_0, s_1, s_2, \ldots}
        | mo= =
        | mr= \sequence {t_0, t_1, t_2, \ldots}
        | rc= where $\ds t_i = \sum_{j \mathop + k \mathop = i} r_j s_k$
}}
{{end-axiom}}
From Polynomial Ring of Sequences is Ring we have that $\struct {S, +, \circ}$ is a ring.
{{Finish|To be proved: a) that the sequences $\tuple {a_0, 0_D, 0_d}$ form a subring $D'$ of $\struct {S, +, \circ}$ isomorphic to $D$, b) the sequence $\tuple {0_D, 1_D, 0_D, 0_D, \dotsc}$ is transcendental over $D'$, and c) that $D' \sqbrk X$ is the whole of $R$. Thus we have constructed $D' \simeq D$. If we now ignore the difference between $a_0 \in D$ and $\tuple {a_0, 0_D, 0_d} \in D'$ so that $D'$ is identified with $D$ the ring $D \sqbrk X$ has been constructed as required.}}
Theorem: Rule of Distribution/Conjunction Distributes over Disjunction/Left Distributive/Formulation 2/Reverse Implication

:$\vdash \paren {\paren {p \land q} \lor \paren {p \land r} } \implies \paren {p \land \paren {q \lor r} }$

Proof:
{{BeginTableau|\vdash \paren {\paren {p \land q} \lor \paren {p \land r} } \implies \paren {p \land \paren {q \lor r} } }}
{{Assumption|1|\paren {p \land q} \lor \paren {p \land r} }}
{{SequentIntro|2|1|p \land \paren {q \lor r}|1|Conjunction is Left Distributive over Disjunction: Formulation 1}}
{{Implication|3||\paren {\paren {p \land q} \lor \paren {p \land r} } \implies \paren {p \land \paren {q \lor r} }|1|2}}
{{EndTableau|qed}}
Category:Rule of Distribution
4xdpwkqew86bfwvoa7yxw9ptss5vflc
Theorem: Eisenstein Integers form Integral Domain

The ring of Eisenstein integers $\struct {\Z \sqbrk \omega, +, \times}$ is an integral domain.

Proof:
By Eisenstein Integers form Subring of Complex Numbers we know that $\struct {\Z \sqbrk \omega, +, \times}$ is a subring of the complex numbers $\C$.
Let $1_\C$ be the unity of $\C$.
Let $1_\omega$ be the unity of $\Z \sqbrk \omega$.
By the Subdomain Test it suffices to show that $1_\C = 1_\omega$.
By Unity of Ring is Unique it suffices to show that $1_\C$ is a unity of $\Z \sqbrk \omega$.
First we note that:
:$\Z \sqbrk \omega = \set {a + b\omega: a, b \in \Z}$
In particular:
:$1_\C \in \Z \sqbrk \omega$
Moreover, by definition, $\Z \sqbrk \omega$ inherits its ring product from $\C$.
For any $\alpha \in \Z \sqbrk \omega$:
:$1_\C \alpha = \alpha 1_\C = \alpha$
in $\C$.
Therefore this identity holds in $\Z \sqbrk \omega$ as well.
{{Qed}}
Category:Number Theory
Category:Examples of Integral Domains
Category:Eisenstein Integers
335lh4rtnhgamtsnweft5ycl35lc3ny
Theorem: Eisenstein Integers form Subring of Complex Numbers

The set of Eisenstein integers $\Z \sqbrk \omega$, under the operations of complex addition and complex multiplication, forms a subring of the set of complex numbers $\C$.

Proof:
We will use the Subring Test.
This is valid, as the set of complex numbers $\C$ forms a field, which is by definition itself a ring.
We note that $\Z \sqbrk \omega$ is not empty, as (for example) $0 + 0 \omega \in \Z \sqbrk \omega$.
Let $a + b \omega, c + d \omega \in \Z \sqbrk \omega$.
Then we have $-\paren {c + d \omega} = -c - d \omega$, and so:
{{begin-eqn}}
{{eqn | l = \paren {a + b \omega} + \paren {-\paren {c + d \omega} }
      | r = \paren {a + b \omega} + \paren {-c - d \omega}
      | c = 
}}
{{eqn | r = \paren {a + \paren {-c} } + \paren {b + \paren {-d} } \omega
      | c = 
}}
{{eqn | r = \paren {a - c} + \paren {b - d} \omega
      | c = 
}}
{{end-eqn}}
We have that $a, b, c, d \in \Z$ and $\Z$ is an integral domain.
Therefore by definition $\Z$ is a ring.
So it follows that $a - c \in \Z$ and $b - d \in \Z$.
Hence $\paren {a - c} + \paren {b - d} \omega \in \Z \sqbrk \omega$.
Now consider $\paren {a + b \omega} \paren {c + d \omega}$.
By the definition of complex multiplication, we have:
:$\paren {a + b \omega} \paren {c + d \omega} = \paren {a c - b d} + \paren {a d + b c} \omega$
As $a, b, c, d \in \Z$ and $\Z$ is a ring, it follows that $a c - b d \in \Z$ and $ad + bc \in \Z$.
Hence:
:$\paren {a + b \omega} \paren {c + d \omega} \in \Z \sqbrk \omega$
So by the Subring Test, $\Z \sqbrk \omega$ is a subring of $\C$.
{{qed}}
Theorem: Norm of Eisenstein Integer

Let $\alpha$ be an Eisenstein integer.
That is:
:$\alpha = a + b \omega$ for some $a, b \in \Z$
where $\omega := e^{2 \pi i /3}$ is a cube root of unity.
Then:
:$\cmod \alpha^2 = a^2 - a b + b^2$
where $\cmod {\, \cdot \,}$ denotes the modulus of a complex number.

Proof:
We find that:
{{begin-eqn}}
{{eqn | l = \cmod \alpha^2
      | r = \alpha \overline \alpha
      | c = Modulus in Terms of Conjugate
}}
{{eqn | r = \paren {a + b \omega} \paren {\overline {a + b \omega} }
      | c = Modulus in Terms of Conjugate
}}
{{eqn | r = \paren {a + b \omega} \paren {\overline a + \overline b \overline \omega}
      | c = Sum of Complex Conjugates and Product of Complex Conjugates
}}
{{eqn | r = \paren {a + b \omega} \paren {a + b \overline \omega}
      | c = Complex Number equals Conjugate iff Wholly Real
}}
{{eqn | r = a^2 + \paren {\omega + \overline \omega} a b + \omega \overline \omega b^2
      | c = 
}}
{{end-eqn}}
By the definition of the polar form of a complex number:
:$\omega = \exp \paren {\dfrac {2 \pi i} 3} = \map \cos {\dfrac {2 \pi} 3} + i \, \map \sin {\dfrac {2 \pi} 3} = -\dfrac 1 2 + i \dfrac {\sqrt 3} 2$
Thus by Sum of Complex Number with Conjugate:
:$\omega + \overline \omega = 2 \cdot \paren {-\dfrac 1 2} = -1$
Also:
{{begin-eqn}}
{{eqn | l = \omega \overline \omega
      | r = \map \exp {\dfrac {2 \pi i} 3} \, \overline {\map \exp {\dfrac {2 \pi i} 3} }
      | c = 
}}
{{eqn | r = \map \exp {\dfrac {2 \pi i} 3} \, \map \exp {-\dfrac {2 \pi i} 3}
      | c = Polar Form of Complex Conjugate
}}
{{eqn | r = \map \exp {\dfrac {2 \pi i} 3 - \dfrac {2 \pi i} 3}
      | c = Exponential of Sum
}}
{{eqn | r = \map \exp 0
      | c = 
}}
{{eqn | r = 1
      | c = Exponential of Zero
}}
{{end-eqn}}
Therefore:
:$\cmod \alpha^2 = a^2 + \paren {\omega + \overline \omega} a b + \omega \overline \omega b^2 = a^2 - a b + b^2$
as required.
{{qed}}
Category:Algebraic Number Theory
kvebuzqg2m7bcaf0j1p9u6cbnkajti3
Theorem: Polynomial Forms over Field form Integral Domain/Formulation 2

Let $\struct {F, +, \circ}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $\GF$ be the set of all polynomials over $\struct {F, +, \circ}$ defined as sequences.
Let polynomial addition and polynomial multiplication be defined as:
:$\forall f = \sequence {a_k} = \tuple {a_0, a_1, a_2, \ldots}, g = \sequence {b_k} = \tuple {b_0, b_1, b_2, \ldots} \in \GF$:
::$f \oplus g := \tuple {a_0 + b_0, a_1 + b_1, a_2 + b_2, \ldots}$
::$f \otimes g := \tuple {c_0, c_1, c_2, \ldots}$ where $\ds c_i = \sum_{j \mathop + k \mathop = i} a_j \circ b_k$
Then $\struct {\GF, \oplus, \otimes}$ is an integral domain.

Proof:
As $\struct {F, +, \circ}$ is a field, it is also by definition a ring.
Thus from Polynomial Ring of Sequences is Ring we have that $\struct {\GF, \oplus, \otimes}$ is a ring.
{{explain|Use an analogous result to Ring of Polynomial Forms is Commutative Ring with Unity to get the CRU bit done}}
From Field is Integral Domain, a field is also by definition an integral domain.
Let $f, g \in \GF$ such that neither $f$ nor $g$ are the null polynomial.
Let:
:$\deg f = m, \deg g = n$
where $\deg$ denotes the degree of $f$ and $g$ respectively.
By Degree of Product of Polynomials over Integral Domain, the degree of $f \times g$ is $m + n$.
Then by definition of polynomial multiplication, its leading coefficient is $a_m \circ b_n$.
As by definition an integral domain has no proper zero divisors:
:$a_m \circ b_n \ne 0_F$.
So, by definition, $f \otimes g$ has a leading coefficient which is not $0_F$.
That is, $f \otimes g$ is not the null polynomial
The result follows by definition of integral domain.
Theorem: Maximal Spectrum of Ring is Nonempty

Let $A$ be a non-trivial commutative ring with unity.
Then its maximal spectrum is non-empty:
:$\operatorname {Max} \Spec A \ne \O$

Proof:
This is a reformulation of Krull's Theorem.
{{qed}}
Theorem: Ring of Polynomial Functions is Commutative Ring with Unity

Let $\struct {R, +, \circ}$ be a commutative ring with unity.
Let $R \sqbrk {\set {X_j: j \in J} }$ be the ring of polynomial forms over $R$ in the indeterminates $\set {X_j: j \in J}$.
Let $R^J$ be the free module on $J$.
Let $A$ be the set of all polynomial functions $R^J \to R$.
Let $\struct {A, +, \circ}$ be the ring of polynomial functions on $R$.
Then $\struct {A, +, \circ}$ is a commutative ring with unity.

Proof:
First we check that the operations of ring product and ring addition are closed in $A$.
Let $Z$ be the set of all multiindices indexed by $J$.
Let:
:$\ds f = \sum_{k \mathop \in Z} a_k \mathbf X^k, \ g = \sum_{k \mathop \in Z} b_k \mathbf X^k \in R \sqbrk {\set {X_j: j \in J} }$.
Under the evaluation homomorphism, $f$ and $g$ map to:
:$\ds A \owns \hat f: \forall x \in R^J: \map {\hat f} x = \sum_{k \mathop \in Z} a_k x^k$
:$\ds A \owns \hat g: \forall x \in R^J: \map {\hat g} x = \sum_{k \mathop \in Z} b_k x^k$
{{explain|Clarification needed on the above link: exactly what the "evaluation homomorphism" is needs to be established.}}
Then the induced pointwise sum of $\hat f$ and $\hat g$ is:
{{begin-eqn}}
{{eqn | l = \map {\hat f} x + \map {\hat g} x
      | r = \sum_{k \mathop \in Z} a_k x^k + \sum_{k \mathop \in Z} b_k x^k
}}
{{eqn | r = \sum_{k \mathop \in Z} \paren {a_k + b_k} x^k
}}
{{eqn | r = \map {\widehat {f + g} } x
      | c = {{Defof|Addition of Polynomial Forms}}
}}
{{end-eqn}}
Thus polynomial functions are closed under ring addition.
The induced pointwise product of $\hat f$ and $\hat g$ is:
{{begin-eqn}}
{{eqn | l = \map {\hat f} x \circ \map {\hat g} x
      | r = \paren {\sum_{k \mathop \in Z} a_k x^k} \circ \paren {\sum_{k \mathop \in Z} a_k x^k}
}}
{{eqn | r = \sum_{k \mathop \in Z} \paren {\sum_{p + q \mathop = k} a_p b_q} \mathbf X^k
}}
{{eqn | r = \map {\widehat {f \circ g} } x
      | c = {{Defof|Multiplication of Polynomial Forms}}
}}
{{end-eqn}}
Thus polynomial functions are closed under ring product.
Finally, we invoke Structure Induced by Ring Operations is Ring, which shows that $\struct {A, +, \circ}$ is a commutative ring with unity.
{{qed}}
Category:Polynomial Theory
cu1qez48f779zij6op3hi56v8279fqy
Theorem: Knaster-Tarski Lemma

Let $\struct {L, \preceq}$ be a complete lattice.
Let $f: L \to L$ be an increasing mapping.
Then $f$ has a smallest fixed point and a greatest fixed point.

Proof:
Let $P = \set {x \in L: x \preceq \map f x}$.
Let $p = \bigvee P$, the supremum of $P$.
Let $x \in P$.
Then by the definition of supremum:
:$x \preceq p$
Since $f$ is increasing:
:$\map f x \preceq \map f p$
By the definition of $P$:
:$x \preceq \map f x$
Thus because $\preceq$ is an ordering, and therefore transitive:
:$x \preceq \map f p$
As this holds for all $x \in P$, $\map f p$ is an upper bound of $P$.
By the definition of supremum:
:$p \preceq \map f p$
As $f$ is increasing:
:$\map f p \preceq \map f {\map f p}$
Thus by the definition of $P$:
:$\map f p \in P$
Since $p$ is the supremum of $P$:
:$\map f p \preceq p$
Since we already know that $p \preceq \map f p$:
:$\map f p = p$
because $\preceq$ is an ordering and therefore antisymmetric.
Thus $p$ is a [[Definition:Fixed Point|fixed p
oint]] of $f$.
We have that $\preceq$ is an ordering, and therefore reflexive.
Thus every fixed point of $f$ is in $P$.
So $p$ is the greatest fixed point of $f$.
Now note that $f$ is also increasing in the dual ordering.
Thus $f$ also has a greatest fixed point in the dual ordering.
That is, it has a least fixed point in the original ordering.
{{qed}}
{{Namedfor|Bronisław Knaster|name2 = Alfred Tarski|cat = Knaster|cat2 = Tarski}}
Theorem: Knaster-Tarski Lemma

Let $\struct {L, \preceq}$ be a complete lattice.
Let $f: L \to L$ be an increasing mapping.
Then $f$ has a smallest fixed point and a greatest fixed point.

Proof:
By the Knaster-Tarski Lemma: Power Set, $f$ has a least fixed point.
Thus it has a fixed point.
{{qed}}
Theorem: Knaster-Tarski Lemma

Let $\struct {L, \preceq}$ be a complete lattice.
Let $f: L \to L$ be an increasing mapping.
Then $f$ has a smallest fixed point and a greatest fixed point.

Proof:
Let $P = \set {x \in \powerset S: x \subseteq \map f x}$.
Let $\ds \bigcup P$ be the union of $P$.
Let $x \in P$.
Then by Set is Subset of Union: General Result:
:$\ds x \subseteq \bigcup P$
Since $f$ is increasing, $\map f x \subseteq \map f {\bigcup P}$.
By definition of $P$, $x \subseteq \map f x$.
Thus $\ds x \subseteq \map f {\bigcup P}$ by Subset Relation is Transitive:
As this holds for all $x \in P$,  by Union is Smallest Superset: General Result:
:$\ds \bigcup P \subseteq \map f {\bigcup P}$
Now since $f$ is increasing:
:$\ds \map f {\bigcup P} \subseteq \map f {\map f {\bigcup P} }$
Thus $\ds \map f {\bigcup P} \in P$ by definition of $P$.
Therefore by Set is Subset of Union: General Result:
:$\ds \map f {\bigcup P} \subseteq \bigcup P$
We have that:
:$\ds \bigcup P \subseteq \map f {\bigcup P}$
Thus by definition of set equality:
:$\ds \map f {\bigcup P} = \bigcup P$
Thus $\ds \bigcup P$ is a fixed point of $f$.
{{qed}}
Theorem: Knaster-Tarski Theorem

Let $\struct {L, \preceq}$ be a complete lattice.
Let $f: L \to L$ be an increasing mapping.
Let $F$ be the set (or class) of fixed points of $f$.
Then $\struct {F, \preceq}$ is a complete lattice.

Proof:
Let $S \subseteq F$.
Let $s = \bigvee S$ be the supremum of $S$.
We wish to show that there is an element of $F$ that succeeds all elements of $S$ and is the smallest element of $F$ to do so.
By the definition of supremum, an element succeeds all elements of $S$ {{iff}} it succeeds $s$.
Let $U = s^\succeq$ be the upper closure of $s$.
Thus we seek the smallest fixed point of $f$ that lies in $U$.
Note that $U = \closedint s \top$, the closed interval between $s$ and the top element of $L$.
First we show that $U$ is closed under $f$.
We have that:
:$\forall a \in S: a \preceq s$
so:
:$a = \map f a \preceq \map f s$
Thus $\map f s$ is an upper bound of $S$.
So by the definition of supremum, $s \preceq \map f s$.
Let $x \in U$.
Then $s \preceq x$.
So:
:$\map f s \preceq \map f x$
Since $s \preceq \map f s$, it follows that:
:$s \preceq \map f x$
so:
:$\map f x \in U$
Thus the restriction of $f$ to $U$ is an increasing mapping from $U$ to $U$.
By Closed Interval in Complete Lattice is Complete Lattice, $\struct {U, \preceq}$ is a complete lattice.
Thus by Knaster-Tarski Lemma, $f$ has a smallest fixed point in $U$.
Thus $S$ has a supremum in $F$.
A similar argument shows that $S$ has an infimum in $F$.
Since this holds for all $S \subseteq F$, it follows that $\struct {F, \preceq}$ is a complete lattice.
{{qed}}
Theorem: Degree of Product of Polynomials over Ring/Corollary 2

Let $\struct {D, +, \circ}$ be an integral domain whose zero is $0_D$.
Let $D \sqbrk X$ be the ring of polynomials over $D$ in the indeterminate $X$.
For $f \in D \sqbrk X$ let $\map \deg f$ denote the degree of $f$.
Then:
:$\forall f, g \in D \sqbrk X: \map \deg {f g} = \map \deg f + \map \deg g$

Proof:
An integral domain is a commutative and unitary ring with no proper zero divisors.
The result follows from Degree of Product of Polynomials over Ring: Corollary 1.
{{qed}}
Theorem: Knaster-Tarski Lemma/Power Set

Let $S$ be a set.
Let $\powerset S$ be the power set of $S$.
Let $f: \powerset S \to \powerset S$ be a $\subseteq$-increasing mapping.
That is, suppose that for all $T, U \in \powerset S$:
:$T \subseteq U \implies \map f T \subseteq \map f U$
Then $f$ has a greatest fixed point and a least fixed point.

Proof:
By Power Set is Complete Lattice, $\struct {\powerset S, \cap, \cup, \subseteq}$ is a complete lattice.
Thus the theorem holds by the Knaster-Tarski Lemma.
{{qed}}
{{Namedfor|Bronisław Knaster|name2 = Alfred Tarski|cat = Knaster|cat2 = Tarski}}