avewright/proofwiki-math huggingface dataset:
Theorem: Maximal Principles are Equivalent to Axiom of Choice

The Maximal Principles are equivalent to the Axiom of Choice.

Proof:
{{ProofWanted|Establish this for each separate one, as and when I reach them in S&F}}
Theorem: Maximal Element of Nest is Greatest Element

Let $A$ be a nest.
Let $x$ be a maximal element of $A$.
Then $x$ is the greatest element of $A$.

Proof:
Let $x$ be a maximal element of $A$.
Let $y \in A$ be arbitrary such that $x \ne y$.
We have by definition of maximal element that:
:$x \not \subset y$
and as $x \ne y$:
:$x \nsubseteq y$
But because $A$ is a nest:
:$x \subseteq y$ or $y \subseteq x$
from which it follows that it must be the case that:
:$y \subseteq x$
As $y$ is arbitrary, the result follows by definition of greatest element.
{{qed}}
Theorem: Non-Empty Set of Type M has Maximal Element

Let $S$ be a non-empty set of sets which is of type $M$.
Then $S$ has a maximal element under the subset relation.

Proof:
Let $S$ be a non-empty set type $M$ set.
Let $x \in S$ be arbitrary.
Then by definition $x$ is a subset of a maximal element of $S$ under the subset relation.
Hence there has to actually ''be'' such a maximal element of $S$ for $x$ to be a subset of.
{{qed}}
Theorem: Axiom of Choice implies Kuratowski's Lemma

Let the Axiom of Choice be accepted.
Then Kuratowski's Lemma holds.

Proof:
We have:
* Axiom of Choice implies Zorn's Lemma
* Zorn's Lemma implies Kuratowski's Lemma.
{{qed}}
Theorem: Closed Set under Chain Unions with Choice Function is of Type M

Let $S$ be a set which is closed under chain unions.
Let there exist a choice function for $S$.
Then $S$ is of type $M$, that is:
:every element of $S$ is a subset of a maximal element of $S$ under the subset relation.

Proof:
Let $S$ be closed under chain unions.
Let $C$ be a choice function for $S$.
For $x \in S$, let $x^*$ be defined as the set of all elements $y$ of $S$ such that $x$ is a proper subset of $y$:
:$\forall x \in S: x^* := \set {y \in S: x \subsetneqq y}$
We have that $x^*$ is empty {{iff}} $x$ is a maximal element of $S$ under the subset relation.
Let us define a progressing mapping $g$ on $S$ as follows:
:$\forall x \in S: \map g x = \begin{cases} x & : \text {$x$ is maximal} \\ \map C {x^*} & : \text {otherwise} \end{cases}$
Thus:
:if $x$ is a maximal element of $S$, then $\map g x = x$
:if $x$ is not a maximal element of $S$, then $x$ is a proper subset of $\map g x$.
By Set which is Superinductive under Progressing Mapping has Fixed Point: Corollary:
:for all $b \in S$, $b$ is a subset of some $x \in S$ such that $x = \map g x$.
This element $x$ is then a maximal element of $S$.
{{qed}}
Theorem: Maximal Element under Subset Relation need not be Greatest Element

Let $A$ be a class.
Let $M \in A$ be a maximal element of $A$ under the subset relation
Then $M$ is not necessarily the greatest element of $A$.

Proof:
Let $A = \set {x, y}$ such that:
:$x = \set \O$
:$y = \set {\set \O}$
Then:
:$x$ and $y$ are both maximal elements of $A$ by definition.
However:
:$x \not \subseteq y$
and:
:$y \not \subseteq x$
and so neither $x$ nor $y$ are the greatest element of $A$.
{{qed}}
Theorem: Sigma-Algebra Generated by Finite Partition is Finite Sub-Sigma-Algebra

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\xi$ be a finite partition of $\Omega$.
Let $\map \sigma \xi$ the generated $\sigma$-algebra by $\xi$.
Then, $\map \sigma \xi$ is a finite sub-$\sigma$-algebra of $\Sigma$.
Furthermore:
:$\ds \map \sigma \xi = \set {\bigcup S: S \subseteq \xi}$

Proof:
Let:
:$\ds \Gamma := \set {\bigcup S: S \subseteq \xi}$
By Power Set of Finite Set is Finite, $\Gamma$ is finite.
Therefore, it suffices to show:
:$\map \sigma \xi = \Gamma$
As $\xi$ is finite,  from (SA3) follows:
:$\map \sigma \xi \supseteq \Gamma$
To conclude the equality, by definition of $\map\sigma\xi$, we need to show that $\Gamma$ is a $\sigma$-algebra.
{{improve|The arguments below are trivial but need more details}}
(SA1) follows from:
:$\ds X = \bigcup \xi \in \Gamma$
(SA2) follows from:
:$\ds \forall S\subseteq\xi : X\setminus\bigcup S = \bigcup \paren {\xi\setminus S} \in \Gamma$
(SA3) follows from:
:$\ds \forall S_1, S_2,\ldots\subseteq\xi : \bigcup _{i=1}^\infty \paren {\bigcup S_i} = \bigcup \paren {\bigcup _{i=1}^\infty S_i} \in \Gamma$
{{qed}}
Category:Probability Theory
Category:Ergodic Theory
ht0329he70jp0z9egqnbqmkv4h4zw0h
Theorem: Properties of Join

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\eta, \gamma$ be finite partitions of $\Omega$.
Then:
:$\map \sigma {\eta \vee \gamma} = \map \sigma \eta \vee \map \sigma \gamma$
where:
:$\map \sigma \cdot$ denotes the generated $\sigma$-algebra
:$\vee$ on the {{LHS}} denotes the join of finite partitions
:$\vee$ on the {{RHS}} denotes the join of finite sub-$\sigma$-algebras

Proof:
{{proofWanted}}
Theorem: Characterization of Almost Everywhere Zero

<onlyinclude>
Let $\struct {X, \Sigma}$ be a measurable space.
Let $\mu$ be a measure on $\struct {X, \Sigma}$.
Let $f : X \to \overline \R$ be a measurable function.
Then:
:$f = 0$ $\mu$-almost everywhere
{{iff}}:
:$\ds \forall A \in \Sigma : \int \paren {\chi_A \cdot f} \rd \mu = 0$
where:
:$\chi_A$ is the characteristic function of $A$

Proof:
=== Necessary condition ===
First, by Measurable Function Zero A.E. iff Absolute Value has Zero Integral:
:$\ds \int \size f \rd \mu = 0$
Let $A\in\Sigma$.
Let $\paren {\chi_A \cdot f}^+$, $\paren {\chi_A \cdot f}^-$ be the positive and negative parts of $\chi_A \cdot f$, respectively.
Observe:
:$\paren {\chi_A \cdot f}^+ \le \size f$
and:
:$\paren {\chi_A \cdot f}^- \le \size f$
Therefore, by Integral of Positive Measurable Function is Monotone:
:$\ds \int \paren {\chi_A \cdot f}^+ \rd \mu \le \int \size f \rd \mu = 0$
and:
:$\ds \int \paren {\chi_A \cdot f}^- \rd \mu \le \int \size f \rd \mu = 0$
This means by definition of integral:
:$\ds \int \paren { \chi_A \cdot f } \rd \mu = 0$.
{{qed|lemma}}
Theorem: Nesthood has Finite Character

Let $P$ be the property of sets defined as:
:$\forall x: \map P x$ denotes that $x$ is a nest.
Then $P$ is of finite character.
That is:
:$x$ is a nest
{{iff}}:
:every finite subset of $x$ is a nest.

Proof:
By definition, a nest $N$ is a class on which $\subseteq$ is a total ordering.
Here we are given that $N$ is a set.
The result follows from Property of being Totally Ordered is of Finite Character.
{{qed}}
Theorem: Nesthood has Finite Character

Let $P$ be the property of sets defined as:
:$\forall x: \map P x$ denotes that $x$ is a nest.
Then $P$ is of finite character.
That is:
:$x$ is a nest
{{iff}}:
:every finite subset of $x$ is a nest.

Proof:
By definition, a nest is a class on which $\subseteq$ is a total ordering.
=== Sufficient Condition ===
Let $x$ be a nest.
Let $y \subseteq x$.
From Restriction of Total Ordering is Total Ordering it follows that $y$ is also a nest.
This holds in particular if $y$ is a finite set.
Hence the result.
{{qed|lemma}}
=== Necessary Condition ===
Suppose that every finite subset of $x$ is a nest.
We have that Subset Relation is Ordering.
It remains to show that $\subseteq$ is total.
Let $y, y' \in x$ be arbitrary.
Since $\set {y, y'}$ is a finite subset of $x$, it is a nest.
Therefore, either $y \subseteq y'$ or $y' \subseteq y$.
Since $y, y'$ were arbitrary, it follows that $x$ is also a nest.
{{qed}}
Theorem: Set whose every Finite Subset is Nest is also Nest

{{explain|We have a set of sets but refer to Definition:Nest (Class Theory)}}
Let $x$ be a set of sets with the property that:
:every finite subset of $x$ is a nest.
Then $x$ is a nest.

Proof:
Let $x$ be a set of sets with the given property.
Let $a, b \in x$ be arbitrary.
Then:
:$\set {a, b} \subseteq x$
and so $\set {a, b}$ is a nest.
That is:
:$a \subseteq b$ or $b \subseteq a$
As $a$ and $b$ are arbitrary, it follows that:
:$\forall a, b \in x: a \subseteq b$ or $b \subseteq a$
{{explain|As per definition, it seems to me that the above line already establishes the definition of nest? What does Subset Relation is Ordering add?}}
The result follows from Subset Relation is Ordering.
{{qed}}
Theorem: Consistency of Logical Formulas has Finite Character

Let $P$ be the property of collections of logical formulas defined as:
:$\forall \FF: \map P \FF$ denotes that $\FF$ is consistent.
Then $P$ is of finite character.
That is:
:$\FF$ is a consistent set of formulas {{iff}} every finite subset of $\FF$ is also a consistent set of formulas.

Proof:
{{ProofWanted|Use Compactness Theorem. And again, the "iff" in the definition of finite character is the interesting part}}
Theorem: Set of Logical Formulas is Inconsistent iff it has Finite Inconsistent Subset

Let $\FF$ be a collection of logical formulas.
Then:
:$\FF$ be inconsistent
{{iff}}:
there exists a finite subset of $\FF$ which it itself inconsistent.

Proof:
=== Sufficient Condition ===
Let $\FF$ be inconsistent.
Then it is possible to assemble a proof in a finite set of statements of a contradiction.
This finite set of statements uses within it a finite subset $\GG \subseteq \FF$ of the logical formulas of $\FF$.
Hence $\GG$ is that inconsistent finite subset of $\FF$ whose existence is proposed.
{{qed|lemma}}
Theorem: Consistent Set of Formulas can be Extended to Maximal Consistent Set

Let $\FF$ be a collection of consistent logical formulas.
Then $\FF$ can be extended to (that is, is a subset of) a maximal consistent set of formulas.

Proof:
{{ProofWanted|This is probably the same as Finitely Satisfiable Theory has Maximal Finitely Satisfiable Extension}}
Theorem: Tukey's Lemma/Formulation 1

Let $S$ be a non-empty set of finite character.
Then $S$ has an element which is maximal with respect to the subset relation.

Proof:
Let $C \subseteq S$ be a chain.
We will show that $\ds \bigcup C \in S$.
Let $x$ be a finite subset of $\ds \bigcup C$.
By the definitions of subset and of union, each element of $x$ is an element of at least one element of $C$.
By the Principle of Finite Choice, there is a mapping $c: x \to C$ such that:
:$\forall a \in x: a \in \map c x$
Then $\map c x$ is a finite subset of $C$.
From Finite Totally Ordered Set is Well-Ordered, $\map c x$ has a greatest element $m \in C \subseteq S$.
Then:
:$x$ is a finite subset of $m$
and:
:$m \in S$
Since $S$ has finite character:
:$x \in S$
We have thus shown that every finite subset of $\ds \bigcup C$ is in $S$.
Since $S$ is of finite character:
:$\ds \bigcup C \in S$
Thus by Zorn's Lemma, $S$ has a maximal element.
{{qed}}
{{AoC||Zorn's Lemma}}
Theorem: Change of Measures Formula for Integrals

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\mu$ and $\nu$ be $\sigma$-finite measures on $\struct {X, \Sigma}$ such that: 
:$\nu$ is absolutely continuous with respect to $\mu$.
Let $g$ be a Radon-Nikodym derivative of $\nu$ with respect to $\mu$.
Let $f : X \to \overline \R$ be a positive $\Sigma$-measurable function.
Then: 
:$\ds \int f \rd \nu = \int \paren {f \cdot g} \rd \mu$
where:
:$f \cdot g$ is the pointwise product of $f$ and $g$
:$\ds \int \cdot \rd \nu$ denotes the integral of a positive $\Sigma$-measurable function with respect to $\nu$.

Proof:
First consider $f$ a positive simple function. 
From Simple Function has Standard Representation, there exists:
:a finite sequence $a_0, \ldots, a_n$ of non-negative real numbers
:a partition $E_0, E_1, \ldots, E_n$ of $X$ into $\Sigma$-measurable sets
such that: 
:$\ds f = \sum_{i \mathop = 0}^n a_i \chi_{E_i}$
Then:
{{begin-eqn}}
{{eqn	| l = \int f \rd \nu
		| r = \int \paren {\sum_{i \mathop = 0}^n a_i \chi_{E_i} } \rd \nu
}}
{{eqn	| r = \sum_{i \mathop = 0}^n \int a_i \chi_{E_i} \rd \nu
		| c = Integral of Positive Measurable Function is Additive
}}
{{eqn	| r = \sum_{i \mathop = 0}^n a_i \int \chi_{E_i} \rd \nu
		| c = Integral of Positive Measurable Function is Positive Homogeneous
}}
{{eqn	| r = \sum_{i \mathop = 0}^n a_i \map \nu {E_i}
		| c = Integral of Characteristic Function: Corollary
}}
{{eqn	| r = \sum_{i \mathop = 0}^n a_i \int_{E_i} g \rd \mu
		| c = {{Defof|Radon-Nikodym Derivative}}
}}
{{eqn	| r = \sum_{i \mathop = 0}^n a_i \int \paren {\chi_{E_i} \cdot g} \rd \mu
		| c = {{Defof|Integral of Positive Measurable Function over Measurable Set}}
}}
{{eqn	| r = \sum_{i \mathop = 0}^n \int \paren {a_i \chi_{E_i} } \cdot g \rd \mu
		| c = Integral of Positive Measurable Function is Positive Homogeneous
}}
{{eqn	| r = \int \paren {\sum_{i \mathop = 0}^n a_i \chi_{E_i} } \cdot g \rd \mu
		| c = Integral of Positive Measurable Function is Additive
}}
{{eqn	| r = \int \paren {f \cdot g} \rd \mu
}}
{{end-eqn}}
Now suppose that $f$ is a general positive $\Sigma$-measurable function.
From Measurable Function is Pointwise Limit of Simple Functions, there exists an increasing sequence $\sequence {f_n}_{n \mathop \in \N}$ of positive simple functions such that: 
:$\ds \map f x = \lim_{n \mathop \to \infty} \map {f_n} x$
for each $x \in X$.
For each $n \in \N$, we have:
:$\ds \int f_n \rd \nu = \int \paren {f_n \cdot g} \rd \mu$
From the Monotone Convergence Theorem (Measure Theory), we have: 
:$\ds \lim_{n \mathop \to \infty} \int f_n \rd \nu = \int f \rd \nu$
Note that $\sequence {f_n \cdot g}_{n \mathop \in \N}$ is an increasing sequence with $f_n \cdot g \to f \cdot g$.
So, from the Monotone Convergence Theorem (Measure Theory), we have:
:$\ds \lim_{n \mathop \to \infty} \int \paren {f_n \cdot g} \rd \mu = \int \paren {f \cdot g} \rd \mu$
So, we have: 
:$\ds \int f \rd \nu = \int \paren {f \cdot g} \rd \mu$
{{qed}}
Category:Radon-Nikodym Derivatives
Category:Change of Measures Formula for Integrals
jibyq29ma0l68j5pp20stpjca43i3ux
Theorem: Positive Part of Pointwise Product of Functions

Let $X$ be a set. 
Let $f, g : X \to \overline \R$ be extended real-valued functions.
Then: 
:$\map {\paren {f \cdot g}^+} x = \begin{cases}\map {f^+} x \map {g^+} x & \map f x \ge 0 \text { and } \map g x \ge 0 \\ \map {f^-} x \map {g^-} x & \map f x \le 0 \text { and } \map g x \le 0 \\ 0 & \text {otherwise}\end{cases}$
for each $x \in X$, where: 
:$f \cdot g$ is the pointwise product of $f$ and $g$
:$\paren {f \cdot g}^+$ denotes the positive part

Proof:
Let $x \in X$ be such that $\map f x \ge 0$ and $\map g x \ge 0$. 
Then:
:$\map {\paren {f \cdot g} } x = \map f x \map g x \ge 0$
From the definition of the positive part, we then have: 
:$\map {\paren {f \cdot g}^+} x = \map f x \map g x$
Now let $x \in X$ be such that $\map f x \le 0$ and $\map g x \le 0$.
Then, we have: 
:$\map {f^-} x = -\map f x$
and:
:$\map {g^-} x = -\map g x$
from the definition of the negative part. 
Then, we have: 
:$\map f x \map g x \ge 0$
So again:
{{begin-eqn}}
{{eqn	| l = \map {\paren {f \cdot g}^+} x
		| r = \map f x \map g x
		| c = {{Defof|Positive Part}}
}}
{{eqn	| r = \paren {-\map {f^-} x} \paren {-\map {g^-} x}
}}
{{eqn	| r = \map {f^-} x \map {g^-} x
}}
{{end-eqn}}
Now suppose that $x \in X$ is such that neither of: 
:$\map f x \ge 0$ and $\map g x \ge 0$ 
or:
:$\map f x \le 0$ and $\map g x \le 0$
are true. 
Then, we have either $\map f x > 0$ and $\map g x < 0$, or $\map f x < 0$ and $\map g x > 0$.
In either case: 
:$\map f x \map g x < 0$
So, from the definition of the positive part, we have: 
:$\map {\paren {f \cdot g}^+} x = 0$ 
{{qed}}
Category:Positive Parts
cmzk2ll97dvihn485rn9s4zd7bisoxf
Theorem: Negative Part of Pointwise Product of Functions

Let $X$ be a set. 
Let $f, g : X \to \overline \R$ be extended real-valued functions.
Then: 
:$\paren {f \cdot g}^- = f^- g^+ + f^+ g^-$
where: 
:$f \cdot g$ is the pointwise product of $f$ and $g$
:$\paren {f \cdot g}^-$ denotes the negative part.

Proof:
We have: 
{{begin-eqn}}
{{eqn	| l = \map f x \map g x
		| r = \paren {\map {f^+} x - \map {f^-} x} \paren {\map {g^+} x - \map {g^-} x}
		| c = Difference of Positive and Negative Parts
}}
{{eqn	| r = \map {f^+} x \map {g^+} x - \map {f^-} x \map {g^+} x - \map {f^+} x \map {g^-} x + \map {f^-} x \map {g^-} x
}}
{{end-eqn}}
Note that we have $\map f x \map g x \le 0$ {{iff}} $\map f x$ and $\map g x$ have the opposite sign.
That is, {{iff}} $\map f x \ge 0$ and $\map g x \le 0$ or $\map f x \le 0$ and $\map g x \ge 0$. 
In the first case, we have $\map {g^+} x = 0$ and $\map {f^-} x = 0$, so:
:$\map {f^+} x \map {g^+} x = \map {f^-} x \map {g^-} x = 0$
In the second case, we have $\map {f^+} x = 0$ and $\map {g^-} x = 0$, so: 
:$\map {f^+} x \map {g^+} x = \map {f^-} x \map {g^-} x = 0$
So, in either case we have: 
:$\map f x \map g x = -\paren {\map {f^-} x \map {g^+} x + \map {f^+} x \map {g^-} x}$
so since: 
:$\map {f^-} x \map {g^+} x + \map {f^+} x \map {g^-} x \ge 0$
we obtain: 
:$\map {\paren {f \cdot g}^-} x = \map {f^-} x \map {g^+} x + \map {f^+} x \map {g^-} x$
if $\map f x \map g x \le 0$. 
If $\map f x \map g x \ge 0$, $\map f x$ and $\map g x$ have the same sign. 
That is, either $\map f x \ge 0$ and $\map g x \ge 0$ or $\map f x \le 0$ and $\map g x \le 0$. 
In the first case, we have $\map {f^-} x = 0$ and $\map {g^-} x = 0$, so: 
:$\map {f^-} x \map {g^+} x + \map {f^+} x \map {g^-} x = \map {\paren {f \cdot g}^-} x = 0$ 
In the second case, we have $\map {f^+} x = 0$ and $\map {g^+} x = 0$, so: 
:$\map {f^-} x \map {g^+} x + \map {f^+} x \map {g^-} x = \map {\paren {f \cdot g}^-} x = 0$
and hence we are done.
{{qed}}
Category:Negative Parts
jbaw9qb95gkbexns4qkgwim27okt12l
Theorem: Swelled Class contains Empty Set

Let $A$ be a swelled class.
Then the empty set is an element of $A$.

Proof:
By definition of swelled class, every subclass of every element of $A$ is also an element of $A$.
Let $x \in A$.
Then by Empty Class is Subclass of All Classes, the empty class is an element of $A$.
By the {{axiom-link|the Empty Set|Class Theory}}, the empty class is a set.
Hence the result.
{{qed}}
Category:Empty Set
Category:Swelled Classes
atuq3nohe0rick3frkmmsgk28emjb9b
Theorem: Class of Finite Character is Swelled

Let $A$ be a class which has finite character.
Then $A$ is a swelled class.

Proof:
Let $x \in A$ and $y \subseteq x$.
Then {{hypothesis}} every finite subset of $y$ is also a finite subset of $x$.
Hence every finite subset of $y$ is in $A$.
Hence again {{hypothesis}} $y \in A$.
{{qed}}
Theorem: Class of Finite Character is Closed under Chain Unions

Let $A$ be a class which has finite character.
Then $A$ is closed under chain unions.

Proof:
Let $C$ be a chain of elements of $A$.
$C$ is a set.
To show that $\bigcup C \in A$ it is sufficient to show that every finite subset of $\bigcup C$ is also an element of $A$.
Let $\set {y_1, y_2, \ldots, y_n}$ be an arbitrary subset of $\bigcup C$.
For each $i \le n$, we have that $y_i$ is an element of some $c_i$ of $C$.
Let $c$ be the greatest element by the subset relation of the sets $\set {c_1, c_2, \ldots, c_n}$.
Then each of the sets $y_1, y_2, \ldots, y_n$ is an element of $c$.
Hence $\set {y_1, y_2, \ldots, y_n} \subseteq c$.
Thus every finite subset of $\bigcup C$ is the subset of some element of $C$,
Hence every finite subset of $\bigcup C$ is the subset of some element of $A$.
Hence by Class of Finite Character is Swelled, every finite subset of $\bigcup C$ is an element of $A$.
So, as $A$ has finite character:
:$\bigcup C \in A$
{{qed}}
Theorem: Kuratowski's Lemma implies Tukey's Lemma

Let Kuratowski's Lemma be accepted as true.
Then Tukey's Lemma holds.

Proof:
Recall Kuratowski's Lemma:
{{:Kuratowski's Lemma/Formulation 2}}{{qed|lemma}}
Recall Tukey's Lemma:
{{:Tukey's Lemma/Formulation 2}}{{qed|lemma}}
So, let us assume Kuratowski's Lemma.
Let $S$ be a non-empty set of finite character.
From Class of Finite Character is Closed under Chain Unions, $S$ is closed under chain unions.
Then by Kuratowski's Lemma:
:every element of $S$ is a subset of a maximal element of $S$ under the subset relation.
Thus it is seen that Tukey's Lemma likewise holds.
{{qed}}
Theorem: Join of Finite Sub-Sigma-Algebras Generates Join of Finite Partitions

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\BB, \CC \subseteq \Sigma$ be finite sub-$\sigma$-algebras.
Then:
:$\map \xi {\BB \vee \CC} = \map \xi \BB \vee \map \xi \CC$
where:
:$\map\xi\cdot$ denotes the generated finite partition
:$\vee$ on the {{LHS}} denotes the join of finite sub-$\sigma$-algebras
:$\vee$ on the {{RHS}} denotes the join of finite partitions

Proof:
{{proofWanted}}
Theorem: Axiom of Choice implies Tukey's Lemma

Let the Axiom of Choice be accepted.
Then Tukey's Lemma holds.

Proof:
Let us assume the truth of the Axiom of Choice.
From Axiom of Choice implies Kuratowski's Lemma, it follows that Kuratowski's Lemma holds.
From Kuratowski's Lemma implies Tukey's Lemma, it follows that Tukey's Lemma holds.
Hence the result.
{{qed}}
Theorem: Set of Finite Character with Choice Function is of Type M

Let $S$ be a set of sets with finite character.
Let there exist a choice function for $S$.
Then $S$ is of type $M$, that is:
:every element of $S$ is a subset of a maximal element of $S$ under the subset relation.

Proof:
Let $S$ be according to the hypothesis.
From Class of Finite Character is Closed under Chain Unions:
:$S$ is closed under chain unions.
From Closed Set under Chain Unions with Choice Function is of Type $M$:
:$S$ is of type $M$.
{{qed}}
Theorem: Set of Subsets of Finite Character of Countable Set is of Type M

Let $D$ be a countable set.
Let $S$ be a set of subsets of $D$ such that $S$ is of finite character.
Then $S$ is of type $M$, that is:
:every element of $S$ is a subset of a maximal element of $S$ under the subset relation.

Proof:
We have that $\ds \bigcup S \subseteq D$.
Hence by Subset of Countable Set is Countable, $\ds \bigcup S$ is itself countable.
Hence from Countable Set has Choice Function, $S$ has a choice function.
The result follows from Set of Finite Character with Choice Function is of Type $M$.
{{qed}}
Theorem: Positive Part of Composition of Functions

Let $\struct {X, \Sigma}$ and $\struct {X', \Sigma'}$ be measurable spaces.
Let $T : X \to X'$ be a $\Sigma/\Sigma'$-measurable mapping.
Let $f : X' \to \overline \R$ be a function.
Then: 
:$\paren {f \circ T}^+ = f^+ \circ T$
where $\paren {f \circ T}^+$ denotes the positive part of $f \circ T$.

Proof:
Let $x \in X$ be such that $\map {\paren {f \circ T} } x = \map f {\map T x} \ge 0$.
Then $\map f {\map T x} = \map {f^+} {\map T x}$ by the definition of the positive part. 
So:
{{begin-eqn}}
{{eqn	| l = \map {\paren {f \circ T}^+} x
		| r = \map {\paren {f \circ T} } x
		| c = {{Defof|Positive Part}}
}}
{{eqn	| r = \map f {\map T x}
}}
{{eqn	| r = \map {f^+} {\map T x}
}}
{{end-eqn}}
Now let $x \in X$ be such that $\map {\paren {f \circ T} } x = \map f {\map T x} < 0$.
Then $\map {f^+} {\map T x} = 0$ and $\map {\paren {f \circ T}^+} x = 0$ by the definition of the positive part.
So: 
:$\map {\paren {f \circ T}^+} x = \map {\paren {f^+ \circ T} } x$
for all $x \in X$.
{{qed}}
Category:Positive Parts
kvyv1xg7plyqyw9ncilkazpzivs0c2o
Theorem: Negative Part of Composition of Functions

Let $\struct {X, \Sigma}$ and $\struct {X', \Sigma'}$ be measurable spaces.
Let $T : X \to X'$ be a $\Sigma/\Sigma'$-measurable mapping.
Let $f : X' \to \overline \R$ be a function.
Then: 
:$\paren {f \circ T}^- = f^- \circ T$
where $\paren {f \circ T}^-$ denotes the positive part of $f \circ T$.

Proof:
Let $x \in X$ be such that $\map {\paren {f \circ T} } x = \map f {\map T x} \le 0$.
Then $\map {f^-} {\map T x} = -\map f {\map T x}$ by the definition of the negative part. 
So:
{{begin-eqn}}
{{eqn	| l = \map {\paren {f \circ T}^-} x
		| r = -\map {\paren {f \circ T} } x
		| c = {{Defof|Negative Part}}
}}
{{eqn	| r = -\map f {\map T x}
}}
{{eqn	| r = \map {f^-} {\map T x}
}}
{{end-eqn}}
Now let $x \in X$ be such that $\map {\paren {f \circ T} } x = \map f {\map T x} \ge 0$.
Then $\map {f^-} {\map T x} = 0$ and $\map {\paren {f \circ T}^-} x = 0$ by the definition of the positive part.
So: 
:$\map {\paren {f \circ T}^-} x = \map {\paren {f^- \circ T} } x$
for all $x \in X$.
{{qed}}
Category:Negative Parts
hbmbw1mu1llhx3xn7g62cdsmqnt031v