avewright/proofwiki-math huggingface dataset:
Theorem: Equivalence of Definitions of Concentration of Complex Measure on Measurable Set

Let $\struct {X, \Sigma}$ be a measurable space.
{{TFAE|def = Concentration of Complex Measure on Measurable Set}}

Proof:
From Characterization of Null Sets of Variation of Complex Measure, we have that: 
:$\map {\size \mu} {E^c} = 0$ {{iff}}:
::for each $\Sigma$-measurable set $A \subseteq E^c$, we have $\map \mu A = 0$.
Hence the desired equivalence. 
{{qed}}
Category:Concentration of Complex Measure on Measurable Set
pacgw5tun3r9qk5xuetqm8vp6szh3ll
Theorem: Lebesgue Decomposition Theorem/Finite Signed Measure

Let $\nu$ be a finite signed measure on $\struct {X, \Sigma}$. 
Then there exist finite signed measures $\nu_a$ and $\nu_s$ on $\struct {X, \Sigma}$ such that: 
:$(1): \quad \nu_a$ is absolutely continuous with respect to $\mu$
:$(2): \quad \nu_s$ and $\mu$ are mutually singular
:$(3): \quad \nu = \nu_a + \nu_s$

Proof:
This follows immediately from Finite Signed Measure is Complex Measure.
{{qed}}
Theorem: Lebesgue Decomposition Theorem/Complex Measure

Let $\nu$ be a complex measure on $\struct {X, \Sigma}$. 
Then there exists complex measures $\nu_a$ and $\nu_s$ on $\struct {X, \Sigma}$ such that: 
:$(1): \quad \nu_a$ is absolutely continuous with respect to $\mu$
:$(2): \quad \nu_s$ and $\mu$ are mutually singular
:$(3): \quad \nu = \nu_a + \nu_s$

Proof:
Let $\cmod \nu$ be the variation of $\nu$.
From Variation of Complex Measure is Finite Measure, $\cmod \nu$ is a finite measure.
Then from Lebesgue Decomposition Theorem for Finite Measures, there exists finite measures $\cmod \nu_a$ and $\cmod \nu_s$ on $\struct {X, \Sigma}$ such that: 
:$(1): \quad \cmod \nu_a$ is absolutely continuous with respect to $\mu$
:$(2): \quad \cmod \nu_s$ and $\mu$ are mutually singular
:$(3): \quad \cmod \nu = \cmod \nu_a + \cmod \nu_s$
More precisely, the proof of this theorem grants that there exists a $\mu$-null set $N \subseteq X$ such that: 
:$\map {\cmod \nu_a} A = \map {\cmod \nu} {N^c \cap A}$
and:
:$\map {\cmod \nu_s} A = \map {\cmod \nu} {N \cap A}$
for each $A \in \Sigma$, with $\cmod \nu_a$ and $\cmod \nu_s$ having the desired properties. 
Let $\nu_a$ be the intersection measure of $\nu$ by $N^c$.
Let $\nu_s$ be the intersection measure of $\nu$ by $N$.
We verify that $\nu_a$ and $\nu_s$ are our desired complex measures. 
From Variation of Intersection Measure, we have:
:$\cmod {\nu_a} = \cmod \nu_a$
and:
:$\cmod {\nu_s} = \cmod \nu_s$ 
Note that $(1)$ is precisely the definition of the complex measure $\nu_s$ being absolutely continuous with respect to $\mu$.
Hence we have $(1)$. 
Note that $(2)$ is precisely the definition of the complex measure $\nu_s$ being mutually singular to $\mu$.
Hence we have $(2)$.
We finally prove $(3)$. 
For each $A \in \Sigma$, $A \cap N$ and $A \cap N^c$ are disjoint with $\paren {A \cap N} \cup \paren {A \cap N^c} = A$, so we have:
:$\map \nu A = \map \nu {A \cap N} + \map \nu {A \cap N^c} = \map {\nu_a} A + \map {\nu_s} A$ 
Hence we have $(3)$. 
{{qed}}
Theorem: Intersection Measure of Finite Measure is Finite Measure

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\mu$ be a finite measure on $\struct {X, \Sigma}$. 
Let $A \in \Sigma$. 
Let $\mu_A$ be the intersection measure of $\mu$ by $A$.
Then $\mu_A$ is a finite measure.

Proof:
From Intersection Measure is Measure, $\mu_A$ is a measure.
Since $\mu$ is a finite measure, we have: 
:$\map \mu X < \infty$ 
Then, we have: 
{{begin-eqn}}
{{eqn	| l = \map {\mu_A} X
		| r = \map \mu {A \cap X}
		| c = {{Defof|Intersection Measure}}
}}
{{eqn	| r = \map \mu A
		| c = Intersection with Subset is Subset
}}
{{eqn	| o = \le
		| r = \map \mu X
		| c = Measure is Monotone
}}
{{eqn	| o = <
		| r = \infty
}}
{{end-eqn}}
So $\mu_A$ is a finite measure.
{{qed}}
Category:Finite Measures
Category:Intersection Measures
qrgi13nbi4096tykwp4d30adyofp1kc
Theorem: Intersection Complex Measure is Complex Measure

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\mu$ be a complex measure on $\struct {X, \Sigma}$. 
Let $F \in \Sigma$.
Let $\mu_F$ be the intersection complex measure of $\mu$ by $F$.
Then $\mu_F$ is a complex measure.

Proof:
Since $\mu$ is a complex measure, we have: 
:$\map \mu E \in \C$
for each $E \in \Sigma$.
So, in particular: 
:$\map \mu {E \cap F} \in \C$
for all $E \in \Sigma$.
That is: 
:$\map {\mu_F} E \in \C$ 
for all $E \in \Sigma$. 
We verify the two conditions required of a complex measure.
We have:
{{begin-eqn}}
{{eqn	| l = \map {\mu_F} \O
		| r = \map \mu {F \cap \O}
		| c = {{Defof|Intersection Complex Measure}}
}}
{{eqn	| r = \map \mu \O
		| c = Intersection with Empty Set
}}
{{eqn	| r = 0
		| c = since $\mu$ is a complex measure
}}
{{end-eqn}}
Now let $\sequence {S_n}_{n \mathop \in \N}$ be a sequence of pairwise disjoint sets in $\Sigma$.
Then, we have: 
{{begin-eqn}}
{{eqn	| l = \map {\mu_F} {\bigcup_{n \mathop = 1}^\infty S_n}
		| r = \map \mu {F \cap \bigcup_{n \mathop = 1}^\infty S_n}
		| c = {{Defof|Intersection Complex Measure}}
}}
{{eqn	| r = \map \mu {\bigcup_{n \mathop = 1}^\infty \paren {F \cap S_n} } 
		| c = Intersection Distributes over Union
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \map \mu {F \cap S_n}
		| c = using countable additivity of $\mu$
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \map {\mu_F} {S_n}
		| c = {{Defof|Intersection Complex Measure}}
}}
{{end-eqn}}
So $\mu$ is a complex measure.
{{qed}}
Category:Complex Measures
Category:Intersection Complex Measures
3rqcp7xijtqyj8cqkfr1jn325lxkd4o
Theorem: Intersection Signed Measure is Signed Measure

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\mu$ be a signed measure on $\struct {X, \Sigma}$. 
Let $F \in \Sigma$.
Let $\mu_F$ be the intersection signed measure of $\mu$ by $F$.
Then $\mu_F$ is a signed measure.

Proof:
Since $\mu$ is a signed measure it takes values in either $\overline \R \setminus \set \infty$ or $\overline \R \setminus \set {-\infty}$.
That is: 
:$\map \mu E \in \overline \R \setminus \set \infty$ for each $E \in \Sigma$
or:
:$\map \mu E \in \overline \R \setminus \set {-\infty}$ for each $E \in \Sigma$.
In particular: 
:$\map {\mu_F} E = \map \mu {E \cap F} \in \overline \R \setminus \set \infty$ for each $E \in \Sigma$
or:
:$\map {\mu_F} E = \map \mu {E \cap F} \in \overline \R \setminus \set {-\infty}$ for each $E \in \Sigma$.
Now we verify the two conditions required of a signed measure.
We have: 
{{begin-eqn}}
{{eqn	| l = \map {\mu_F} \O
		| r = \map \mu {F \cap \O}
		| c = {{Defof|Intersection Signed Measure}}
}}
{{eqn	| r = \map \mu \O
		| c = Intersection with Empty Set
}}
{{eqn	| r = 0
		| c = {{Defof|Signed Measure}}
}}
{{end-eqn}}
Now let $\sequence {S_n}_{n \mathop \in \N}$ be a sequence of pairwise disjoint sets in $\Sigma$.
Then, we have: 
{{begin-eqn}}
{{eqn	| l = \map {\mu_F} {\bigcup_{n \mathop = 1}^\infty S_n}
		| r = \map \mu {F \cap \bigcup_{n \mathop = 1}^\infty S_n}
		| c = {{Defof|Intersection Signed Measure}}
}}
{{eqn	| r = \map \mu {\bigcup_{n \mathop = 1}^\infty \paren {F \cap S_n} } 
		| c = Intersection Distributes over Union
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \map \mu {F \cap S_n}
		| c = using countable additivity of $\mu$
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \map {\mu_F} {S_n}
		| c = {{Defof|Intersection Signed Measure}}
}}
{{end-eqn}}
So $\mu$ is a signed measure.
{{qed}}
Category:Signed Measures
Category:Intersection Signed Measures
3snnreyqvid3jkdrqkdpr2me5qr6u5p
Theorem: Set of Finite Character with Choice Function is Type M

Let $S$ be a set of sets of finite character.
Let $S$ have a choice function $C$ for its union $\ds \bigcup 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:
By Class of Finite Character is Swelled,  a set of finite character is swelled.
By Class of Finite Character is Closed under Chain Unions a set of finite character is closed under chain unions.
The result follows from Swelled Set which is Closed under Chain Unions with Choice Function is Type $M$.
{{qed}}
Theorem: Set of Finite Character with Countable Union is Type M

Let $S$ be a set of sets of finite character.
Let its union $\bigcup S$ be countable.
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:
By Countable Set has Choice Function, $S$ has a choice function.
The result follows from Set of Finite Character with Choice Function is Type $M$.
{{qed}}
Theorem: Set of Finite Character with Countable Union is Type M

Let $S$ be a set of sets of finite character.
Let its union $\bigcup S$ be countable.
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 a set of sets of finite character whose union $\bigcup S$ is countable.
Let $D := \bigcup S$ be enumerated as:
:$D = \set {d_1, d_2, \ldots, d_n, d_{n + 1}, \ldots}$
Let $b \in S$ be arbitrary.
From the Principle of Recursive Definition, we can generate a countable sequence of elements of $S$ as follows:
Let $b_0 := b$.
Let it be assumed that $b_n$ has been defined.
Then we take:
:$b_{n + 1} := \begin{cases} b_n \cup \set {d_n} & : \text {if $b_n \cup \set {d_n}$ is an element of $S$} \\ b_n & : \text {otherwise} \end{cases}$
Let $C$ be the set defined as
:$C := \set {b_0, b_1, \ldots, b_n, b_{n + 1}, \ldots}$
From Increasing Sequence of Sets forms Nest, $C$ is a nest which, as $C$ is a set, is in fact a chain.
Hence $\bigcup C \in S$.
From Union of Chain in Set of Finite Character with Countable Union is Maximal Element, $\bigcup C$ is a maximal element of $S$ under the subset relation.
Thus $b$ is a subset of a maximal element of $S$ under the subset relation.
As $b$ is arbitrary, the result follows.
{{qed}}
Theorem: Consistent Set of Logical Formulas is Subset of Maximally Consistent Set

Let $\LL$ be a formal language used in the field of symbolic logic.
Let $\FF$ be the set of logical formulas of $\LL$.
Let $\FF$ be countable.
Let $S$ be a consistent subset of $\FF$.
Then $S$ is a subset of some maximal consistent set of formulas.

Proof:
{{ProofWanted|This may be the same as Consistent Set of Formulas can be Extended to Maximal Consistent Set. Smullyan and Fitting are vague here. They may be trying to state Lindenbaum's Lemma, but if this and that are equivalent is not clear.}}
Theorem: Union of Chain in Set of Finite Character with Countable Union is Maximal Element

Let $S$ be a set of sets of finite character.
Let its union $\ds \bigcup S$ be countable.
Then $\ds \bigcup S$ is a maximal element of $S$ under the subset relation.

Proof:
Let $S$ be as {{hypothesis}}.
{{AimForCont}} $\ds \bigcup S$ is not a maximal element of $S$ under the subset relation.
Then:
:$\exists T \subseteq S: \ds \bigcup S \subsetneqq T$
Thus:
:$\exists x \in S: x \ne \ds \bigcup S$
{{ProofWanted|need to ponder this, decide exactly what it's saying and what I can assume}}
Theorem: Finite Signed Measure is Complex Measure

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\mu$ be a finite signed measure on $\struct {X, \Sigma}$. 
Then $\mu$ is a complex measure on $\struct {X, \Sigma}$.

Proof:
Let $\tuple {\mu^+, \mu^-}$ be the Jordan decomposition of $\mu$.
Then: 
:$\mu = \mu^+ - \mu^-$
for measures $\mu^+$ and $\mu^-$. 
From Jordan Decomposition of Finite Signed Measure, $\mu^+$ and $\mu^-$ are finite measures.
Then, for each $A \in \Sigma$, we have:
{{begin-eqn}}
{{eqn	| l = \cmod {\map \mu A}
		| o = \le
		| r = \map {\mu^+} A + \map {\mu^-} A
		| c = Absolute Value of Signed Measure Bounded Above by Variation
}}
{{eqn	| o = \le
		| r = \map {\mu^+} X + \map {\mu^-} X
		| c = Measure is Monotone
}}
{{eqn	| o = <
		| r = \infty
		| c = {{Defof|Finite Measure}}
}}
{{end-eqn}}
So $\mu$ takes only real values.
That is, $\mu$ takes values in $\C$. 
Since $\mu$ is a signed measure, we have: 
:$\map \mu \O = 0$
and: 
:for each sequence $\sequence {S_n}_{n \mathop \in \N}$ of pairwise disjoint $\Sigma$-measurable sets we have: 
::$\ds \map \mu {\bigcup_{n \mathop = 1}^\infty S_n} = \sum_{n \mathop = 1}^\infty \map \mu {S_n}$
So $\mu$ is a complex measure.
{{qed}}
Category:Finite Signed Measures
Category:Complex Measures
hqvr100234q1bvh8c4001toip731pct
Theorem: Distribution Function of Finite Signed Borel Measure is of Bounded Variation

Let $\mu$ be a finite signed Borel measure on $\R$.
Let $F_\mu$ be the distribution function of $\mu$. 
Then $F_\mu$ is of bounded variation.

Proof:
Let $\SS$ be a non-empty finite subset of $\R$. 
Write: 
:$\SS = \set {x_0, x_1, \ldots, x_n}$
with:
:$x_0 < x_1 < x_2 < \cdots < x_{n - 1} < x_n$
Then, we have: 
{{begin-eqn}}
{{eqn	| l = \sum_{i \mathop = 1}^n \size {\map {F_\mu} {x_i} - \map {F_\mu} {x_{i - 1} } }
		| r = \sum_{i \mathop = 1}^n \size {\map \mu {\hointl {-\infty} {x_i} } - \map \mu {\hointl {-\infty} {x_{i - 1} } } }
		| c = {{Defof|Distribution Function of Finite Signed Borel Measure}}
}}
{{eqn	| r = \sum_{i \mathop = 1}^n \size {\map \mu {\hointl {-\infty} {x_i} \setminus \hointl {-\infty} {x_{i - 1} } } }
		| c = Measure of Set Difference with Subset: Signed Measure
}}
{{eqn	| r = \sum_{i \mathop = 1}^n \size {\map \mu {\hointl {x_{i - 1} } {x_i} } }
}}
{{eqn	| o = \le
		| r = \size {\map \mu {\hointl {-\infty} {x_0} } } + \sum_{i \mathop = 1}^n \size {\map \mu {\hointl {x_{i - 1} } {x_i} } } + \size {\map \mu {\hointr {x_n} \infty} }
}}
{{end-eqn}}
Note that: 
:$\set {\hointl {-\infty} {x_0}, \hointl {x_0} {x_1}, \hointl {x_1} {x_2}, \ldots, \hointl {x_{n - 1} } {x_n}, \hointr {x_n} \infty}$ is a partition of $\R$ into Borel sets.
So from Definition 2 of the variation of a signed measure, we have: 
:$\ds \size {\map \mu {\hointl {-\infty} {x_0} } } + \sum_{i \mathop = 1}^n \size {\map \mu {\hointl {x_{i - 1} } {x_i} } } + \size {\map \mu {\hointr {x_n} \infty} } \le \map {\size \mu} \R$ 
where $\size \mu$ is the variation of $\mu$.
From Signed Measure Finite iff Finite Total Variation, we have: 
:$\map {\size \mu} \R < \infty$
So, using the notation from the definition of bounded variation, for all non-empty finite subset of $\R$, $\SS$, we have:
:$\map {V_f^\ast} {\SS; I} \le M = \map {\size \mu} \R$
So $f$ is of bounded variation.
{{qed}}
Theorem: Measure of Set Difference with Subset/Signed Measure

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\mu$ be a signed measure on $\struct {X, \Sigma}$.
Let $S, T \in \Sigma$ be such that $S \subseteq T$ with $\size {\map \mu S} < \infty$.
Then: 
:$\map \mu {T \setminus S} = \map \mu T - \map \mu S$

Proof:
Let $\struct {\mu^+, \mu^-}$ be the Jordan decomposition of $\mu$.
Then, since: 
:$\size {\map \mu S} < \infty$
We have: 
:$\map {\mu^+} S < \infty$ and $\map {\mu^-} S < \infty$
Then, we have: 
{{begin-eqn}}
{{eqn	| l = \map \mu {T \setminus S}
		| r = \map {\mu^+} {T \setminus S} - \map {\mu^-} {T \setminus S}
		| c = {{Defof|Jordan Decomposition}}
}}
{{eqn	| r = \paren {\map {\mu^+} T - \map {\mu^+} S} - \paren {\map {\mu^-} T - \map {\mu^-} S}
		| c = Measure of Set Difference with Subset
}}
{{eqn	| r = \paren {\map {\mu^+} T - \map {\mu^-} T} - \paren {\map {\mu^+} S - \map {\mu^-} S}
}}
{{eqn	| r = \map \mu T - \map \mu S
		| c = {{Defof|Jordan Decomposition}}
}}
{{end-eqn}}
{{qed}}
Category:Measure of Set Difference with Subset
Category:Signed Measures
8hzgg1qrwpotky4anyoofqk62cxyrhb
Theorem: Signed Measure Finite iff Finite Total Variation

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\mu$ be a signed measure on $\struct {X, \Sigma}$. 
Let $\size \mu$ be the variation of $\mu$. 
Then $\mu$ is finite {{iff}}:
:$\map {\size \mu} X < \infty$

Proof:
=== Sufficient Condition ===
Suppose that: 
:$\map {\size \mu} X < \infty$
Then, from Absolute Value of Signed Measure Bounded Above by Variation, we have: 
:$\size {\map \mu X} \le \map {\size \mu} X$
so:
:$\size {\map \mu X} < \infty$
So $\mu$ is finite.
{{qed|lemma}}
Theorem: Measure of Limit of Decreasing Sequence of Measurable Sets

Let $\struct {X, \Sigma, \mu}$ be a measure space. 
Let $E \in \Sigma$.
Let $\sequence {E_n}_{n \mathop \in \N}$ be an decreasing sequence of $\Sigma$-measurable sets such that: 
:$E_n \downarrow E$ 
where $E_n \downarrow E$ denotes the limit of decreasing sequence of sets.
Suppose also that $\map \mu {E_1} < \infty$. 
Then: 
:$\ds \map \mu E = \lim_{n \mathop \to \infty} \map \mu {E_n}$

Proof:
From Relative Complement of Decreasing Sequence of Sets is Increasing, we have: 
:$\sequence {E_1 \setminus E_n}_{n \mathop \in \N}$ is increasing.
Further, we have: 
{{begin-eqn}}
{{eqn	| l = \bigcup_{n \mathop = 1}^\infty \paren {E_1 \setminus E_n}
		| r = E_1 \setminus \paren {\bigcap_{n \mathop = 1}^\infty E_n}
		| c = De Morgan's Law for Set Differences: General Case
}}
{{eqn	| r = E_1 \setminus E
		| c = {{Defof|Limit of Decreasing Sequence of Sets}}
}}
{{end-eqn}}
so:
:$E_1 \setminus E_n \uparrow E_1 \setminus E$ 
So, from Measure of Limit of Increasing Sequence of Measurable Sets, we have: 
:$\ds \map \mu {E_1 \setminus E} = \lim_{n \mathop \to \infty} \map \mu {E_1 \setminus E_n}$
From Measure of Set Difference with Subset, we have: 
:$\ds \map \mu {E_1} - \map \mu E = \lim_{n \mathop \to \infty} \paren {\map \mu {E_1} - \map \mu {E_n} }$
since $\map \mu {E_1} < \infty$. 
From the Difference Rule for Real Sequences, we then have: 
:$\ds \map \mu {E_1} - \map \mu E = \map \mu {E_1} - \lim_{n \mathop \to \infty} \map \mu {E_n}$
giving:
:$\ds \map \mu E = \lim_{n \mathop \to \infty} \map \mu {E_n}$ 
{{qed}}
Theorem: Relative Complement of Decreasing Sequence of Sets is Increasing

Let $X$ be a set.
Let $\sequence {E_n}_{n \mathop \in \N}$ be a decreasing sequence of sets in $X$. 
Then $\sequence {X \setminus E_n}_{n \mathop \in \N}$ is an increasing sequence of sets in $X$.

Proof:
Since $\sequence {E_n}_{n \mathop \in \N}$ is decreasing, we have: 
:$E_{n + 1} \subseteq E_n$ for each $n \in \N$. 
From Relative Complement inverts Subsets, we then have: 
:$X \setminus E_n \subseteq X \setminus E_{n + 1}$ for each $n \in \N$. 
So $\sequence {X \setminus E_n}_{n \mathop \in \N}$ is an increasing sequence of sets in $X$.
{{qed}}
Category:Increasing Sequences of Sets
Category:Relative Complement
Category:Decreasing Sequences of Sets
i2cceai5mmnosrj013yglj7t6qm6gk0
Theorem: Limit of Tail of Decreasing Sequence of Sets

Let $X$ be a set.
Let $\sequence {E_n}_{n \mathop \in \N}$ be a decreasing sequence of subsets of $X$ such that: 
:$E_n \downarrow E$ 
where $E_n \downarrow E$ denotes the limit of decreasing sequence of sets.
Then for each $m \in \N$ we have: 
:$E_{n + m} \downarrow E$

Proof:
Let $m \in \N$.
From Tail of Decreasing Sequence of Sets is Decreasing, we have: 
:$\sequence {E_{n + m} }_{n \mathop \in \N}$ is a decreasing sequence of sets.
Since: 
:$E_n \downarrow E$
we have: 
:$\ds \bigcap_{n \mathop = 1}^\infty E_n = E$
We show that: 
:$\ds \bigcap_{n \mathop = 1}^\infty E_{n + m} = E$
That is: 
:$\ds \bigcap_{n \mathop = m + 1}^\infty E_n = E$
Clearly we have: 
:$\ds \bigcap_{n \mathop = 1}^\infty E_n \subseteq \bigcap_{n \mathop = m + 1}^\infty E_n$
from Intersection is Decreasing.
Now let: 
:$\ds x \in \bigcap_{n \mathop = m + 1}^\infty E_n$
Then: 
:$x \in E_n$ for all $n \in \N$ for all $n \ge m + 1$
and in particular: 
:$x \in E_{m + 1}$ 
Since $\sequence {E_n}_{n \mathop \in \N}$ is a decreasing sequence of sets, we have: 
:$E_{m + 1} \subseteq E_n$ for all $n \in \N$ with $n < m + 1$.
So, we actually have: 
:$x \in E_n$ for all $n \in \N$.
So, from the definition of set intersection, we have: 
:$\ds x \in \bigcap_{n \mathop = 1}^\infty E_n$
So, from the definition of set inclusion, we have: 
:$\ds \bigcap_{n \mathop = m + 1}^\infty E_n \subseteq \bigcap_{n \mathop = 1}^\infty E_n$
So we have: 
:$\ds \bigcap_{n \mathop = 1}^\infty E_{n + m} = E$
{{qed}}
Category:Limits of Sets
Category:Decreasing Sequences of Sets
r8eegrt5qc4wgr8tg6rooolusarwedh
Theorem: Tail of Decreasing Sequence of Sets is Decreasing

Let $X$ be a set.
Let $\sequence {E_n}_{n \mathop \in \N}$ be a decreasing sequence of subsets of $X$.
Then for each $m \in \N$ we have:
:$\sequence {E_{n + m} }_{n \mathop \in \N}$ is a decreasing sequence of sets.

Proof:
Since $\sequence {E_n}_{n \mathop \in \N}$ is an decreasing sequence of sets, we have: 
:$E_{n + 1} \subseteq E_n$ for each $n \in \N$.
Swapping $n$ for $n + m$, this in particular gives:
:$E_{n + m + 1} \subseteq E_{n + m}$ for each $n \in \N$.
So $\sequence {E_{n + m} }_{n \mathop \in \N}$ is a decreasing sequence of sets.
{{qed}}
Category:Decreasing Sequences of Sets
m95lxmgpp5wqkpu1z0kpmlt22fpu0bf
Theorem: Measure of Limit of Decreasing Sequence of Measurable Sets/Corollary

Let $F \in \Sigma$.
Let $\sequence {F_n}_{n \mathop \in \N}$ be an decreasing sequence of $\Sigma$-measurable sets such that: 
:$F_n \downarrow F$ 
where $F_n \downarrow F$ denotes the limit of decreasing sequence of sets.
Suppose also that $\map \mu {F_m} < \infty$ for some $m \in \N$. 
Then: 
:$\ds \map \mu F = \lim_{n \mathop \to \infty} \map \mu {F_n}$

Proof:
Define the sequence $\sequence {E_n}_{n \mathop \in \N}$ by: 
:$E_n = F_{m + n}$ 
Then from Tail of Decreasing Sequence of Sets is Decreasing:
:$\sequence {E_n}_{\mathop \in \N}$ is an decreasing sequence of $\Sigma$-measurable sets.
From Limit of Tail of Decreasing Sequence of Sets, we have: 
:$E_n \downarrow F$
with: 
:$\map \mu {E_1} = \map \mu {F_{m + 1} }$
Since $\sequence {F_n}_{n \mathop \in \N}$ is decreasing, we have: 
:$F_{m + 1} \subseteq F_m$
So from Measure is Monotone, we have: 
:$\map \mu {F_{m + 1} } \le \map \mu {F_m} < \infty$
so:
:$\map \mu {E_1} < \infty$
Then:
{{begin-eqn}}
{{eqn	| l = \map \mu F
		| r = \lim_{n \mathop \to \infty} \map \mu {E_n}
		| c = Measure of Limit of Decreasing Sequence of Measurable Sets
}}
{{eqn	| r = \lim_{n \mathop \to \infty} \map \mu {F_{n + m} }
}}
{{eqn	| r = \lim_{n \mathop \to \infty} \map \mu {F_n}
		| c = Tail of Convergent Sequence
}}
{{end-eqn}}
{{qed}}
Category:Measure of Limit of Decreasing Sequence of Measurable Sets
bo3ujz1ck7769dt1biv9fzzqyu4l4ak
Theorem: Distribution Function of Finite Borel Measure is Bounded

Let $\mu$ be a finite Borel measure on $\R$.
Let $F_\mu$ be the distribution function of $\mu$.
Then $F_\mu$ is bounded.

Proof:
Let $x \in \R$.
Then: 
:$\O \subseteq \hointl {-\infty} x \subseteq \R$
Then, from Measure is Monotone we have: 
:$\map \mu \O \le \map \mu {\hointl {-\infty} x} \le \map \mu \R$
From Empty Set is Null Set, we have: 
:$\map \mu \O = 0$
Since $\mu$ is a finite measure, we have: 
:$\map \mu \R < \infty$
So, we have: 
:$0 \le \map \mu {\hointl {-\infty} x} \le \map \mu \R < \infty$
So:
:$0 \le \map {F_\mu} x \le \map \mu \R$ for each $x \in \R$. 
{{qed}}
Theorem: Distribution Function of Finite Borel Measure is Increasing

Let $\mu$ be a finite Borel measure on $\R$.
Let $F_\mu$ be the distribution function of $\mu$.
Then $F_\mu$ is an increasing function.

Proof:
Let $x, y \in \R$ be such that $x \le y$.
Then: 
:$\hointl {-\infty} x \subseteq \hointl {-\infty} x$
So, from Measure is Monotone:
:$\map \mu {\hointl {-\infty} x} \le \map \mu {\hointl {-\infty} y}$
That is: 
:$\map {F_\mu} x \le \map {F_\mu} y$ whenever $x \le y$.
So $F_\mu$ is an increasing function.
{{qed}}