avewright/proofwiki-math huggingface dataset:
Theorem: Borel-Carathéodory Lemma/Lemma

:$\ds \forall n \in \Z_{\ge 1} : \quad \frac {\cmod {\map {f^{\paren n} } 0} }{ n! } \le \frac {2 M} {R^n}$

Proof:
By Cauchy Integral Theorem:
:$\ds \forall k \in \Z_{\ge 0} : \quad \oint_{\partial D} z^{k-1} \map f z \rd z = 0$
Parametrizing $\partial D$ by $R e^{2 \pi i t}$:
:$\ds \forall k \in \Z_{\ge 0} : \quad \int _0^1 e^{2\pi i k t} \map f {R e^{2 \pi ikt} } \rd t = 0$
On the other hand:
{{begin-eqn}}
{{eqn | l = \map {f^{\paren n} } 0
      | r = \frac {n!} {2 \pi i} \oint_{\partial D} \frac {\map f z} {z^{n + 1} } \rd z
}}
{{eqn | r = \frac {n!} {2 \pi i} \int_0^1 \frac {\map f {R e^{2 \pi i t} } } { \paren {R e^{2 \pi i t} }^{n+1} } \paren {2 \pi i} R e^{2 \pi i t} \rd t
      | c = Parametrize $\partial D$ by $R e^{2 \pi i t}$
}}
{{eqn | r = \frac {n!}{R^n} \int_0^1 e^{- 2 \pi i n t} \map f {R e^{2 \pi i t} } \rd t
      | c = Cauchy's Integral Formula
}}
{{end-eqn}}
Let $\theta_n := \map \arg {\map {f^{\paren n} } 0}$.
Then:
{{begin-eqn}}
{{eqn | l = \cmod {\map {f^{\paren n} } 0}
      | r = e^{-\theta_n i} \map {f^{\paren n} } 0
}}
{{eqn | r = \frac {n!}{R^n} \int_0^1 \map f {R e^{2 \pi i t} } e^{- \paren {2 \pi n t + \theta_n} i} \rd t
}}
{{end-eqn}}
Since:
:$\ds \int_0^1 \map f {R e^{2 \pi i t} } \paren {2 + e^{\paren {2 \pi n t + \theta_n} i } } \rd t = 0$
we have:
{{begin-eqn}}
{{eqn | l = \cmod {\map {f^{\paren n} } 0}
      | r = \frac {n!}{R^n} \int_0^1 \map f {R e^{2 \pi i t} } \paren {2 + e^{\paren {2 \pi n t + \theta_n} i } + e^{- \paren {2 \pi n t + \theta_n} i } } \rd t
}}
{{eqn | r = \frac {2 n!}{R^n} \int_0^1 \map f {R e^{2 \pi i t} } \paren {1 + \map \cos { 2 \pi n t + \theta_n } } \rd t
}}
{{eqn | r = \frac {2 n!}{R^n} \int_0^1 \map \Re {\map f {R e^{2 \pi i t} } } \paren {1 + \map \cos { 2 \pi n t + \theta_n } } \rd t
}}
{{eqn | o = \le
      | r = \frac {2 M n!}{R^n} \int_0^1 1 + \map \cos { 2 \pi n t + \theta_n  } \rd t
}}
{{eqn | r = \frac {2 M n!}{R^n}
}}
{{end-eqn}}
{{qed}}
Category:Complex Analysis
qivaehtct0688vlv4bmkh4a8c6hfhpl
Theorem: Content of Finite Set of Rectangles not Less than Covered Subrectangles

Let $S$ be a finite set of closed $n$-rectangles.
Let $\RR$ be a closed $n$-rectangle that contains every rectangle in $S$.
Let:
:$P = \tuple {P_1, \dotsc, P_n}$
be a subdivision of $\RR$ such that for every:
:$\ds R = \prod_{i \mathop = 1}^n \closedint {a_i} {b_i} \in S$
we have that:
:$a_i, b_i \in P_i$
That is, the endpoints $a_i$ and $b_i$ are elements of the finite subdivision $P_i$.
Let $Q$ be the set of subrectangles of $P$ that are contained in some rectangle in $S$.
Then:
:$\ds \sum_{R \mathop \in S} \map V R \ge \sum_{R \mathop \in Q} \map V R$
where $\map V R$ denotes the content of the rectangle $R$.

Proof:
{{WIP}}
apyo4f6noaqs5oem3dn8fbmgqddd3u3
Theorem: Meet Irreducible Element Induced by Completely Prime Filter

Let $\struct{L, \vee, \wedge, \preceq}$ be a frame.
Let $\top$ denote the greatest element of $L$.
Let $p$ be a completely prime filter of $L$.
Let:
:$b = \bigvee \set{a \in L : a \notin p}$
where:
:$\bigvee \set{a \in L : a \notin p}$ denotes the supremum of the set $\set{a \in L : a \notin p}$
Then:
:$b$ is a meet irreducible element not equal to $\top$

Proof:
Let: 
:$x, y \in S : x \wedge y = b$
By definition of infimum:
:$b \preceq x$
:$b \preceq y$
By the contrapositive statement of the definition of completely prime filter:
:$b \notin p$
By the contrapositive statement of filter axiom $(2)$:
:either $x \notin p$ or $y \notin p$
By definition of supremum:
:either $x \preceq b$ or $y \preceq b$
By ordering axiom $(3)$:
:either $x = b$ or $y = b$
The result follows by definition of meet irreducible element.
{{qed}}
Category:Completely Prime Filters
Category:Meet Irreducible Elements
6lc8p4048g32pb45xrakd6n400mnrzi
Theorem: Completely Prime Filter Induced by Meet Irreducible Element

Let $\struct{L, \vee, \wedge, \preceq}$ be a frame.
Let $b$ be a meet-irreducible element of $L$.
Let:
:$p = \set{a \in L : a \npreceq b}$
Then:
:$p$ is a completely prime filter of $L$.

Proof:
From meet irreducible element, it is sufficient to show:
:$(1)\quad\forall A \subseteq L : \bigvee A \in p \iff \paren{\exists a \in A : a \in p}$
:$(2)\quad\forall $ finite $A \subseteq L : \bigwedge A \in p \iff \paren{\forall a \in A : a \in p}$
where:
:* $\bigvee A$ denotes the supremum of $A$ in $L$
:* $\bigwedge A$ denotes the infimum of $A$ in $L$
By definition of $p$, it is sufficient to show:
:$(1')\quad\forall A \subseteq L : \bigvee A \npreceq b \iff \paren{\exists a \in A : a \npreceq b}$
:$(2')\quad\forall $ finite $A \subseteq L : \bigwedge A \npreceq b \iff \paren{\forall a \in A : a \npreceq b}$
Theorem: Characterization of Meet Irreducible Element

Let $\struct{S, \wedge, \preceq}$ be a meet semilattice.
Let $z \in S$.
Then:
:$z$ is meet irreducible
{{iff}}
:$\forall x, y \in S : \leftparen{z \prec x}$ and $\rightparen{z \prec y} \implies \paren{ z \prec x \wedge y}$
where $z \prec x$ denotes that $z \preceq x$ and $z\neq x$.

Proof:
=== Necessary Condition ===
Let $z$ be a meet irreducible element.
Let:
:$x, y \in S : \leftparen{z \prec x}$ and $\rightparen{z \prec y}$
We have:
:$z \ne x$
:$z \ne y$
By definition of meet irreducible element:
:$z \ne x \wedge y$
By definition of infimum:
:$z \preceq x \wedge y$
Hence:
:$z \prec x \wedge y$
The result follows.
{{qed|lemma}}
Theorem: Characterization of Join Irreducible Element

Let $\struct{S, \vee, \preceq}$ be a join semilattice.
Let $z \in S$.
Then:
:$z$ is join-irreducible
{{iff}}
:$\forall x, y \in S : \leftparen{x \prec z}$ and $\rightparen{y \prec z} \implies \paren{x \vee y \prec z}$
where $x \prec z$ denotes that $x \preceq z$ and $x \neq z$.

Proof:
By Dual Pairs (Order Theory):
* join semilattice is dual to meet semilattice.
* join irreducible element is dual to meet irreducible element.
* join is dual to meet.
* succeeds is dual to precedes.
Thus the theorem holds by the duality principle applied to Characterization of Meet Irreducible Element.
{{qed}}
Category:Join Irreducible Elements
ercs38vruga4byhgz1xge2edub0dn6i
Theorem: Join Prime Element is Join Irreducible

Let $\struct{S, \vee, \preceq}$ be a join semilattice.
Let $z \in S$ be a join-prime element.
Then:
:$z$ is join-irreducible

Proof:
By Dual Pairs (Order Theory):
* join semilattice is dual to meet semilattice.
* join prime element is dual to meet prime element.
* join irreducible element is dual to meet irreducible element.
Thus the theorem holds by the duality principle applied to Characterization of Meet Irreducible Element.
{{qed}}
Category:Join Prime Elements
Category:Join Irreducible Elements
e9bsuakn5ltuuiuy35m3z69l5bihkwv
Theorem: Join Prime Element iff Join Irreducible in Distributive Lattice

Let $\struct {S, \vee, \wedge, \preceq}$ be a distributive lattice.
Let $z \in S$.
Then:
:$z$ is join-irreducible
{{iff}}
:$z$ is join-prime

Proof:
By Dual Pairs (Order Theory):
* join prime element is dual to meet prime element.
* join irreducible element is dual to meet irreducible element.
Thus the theorem holds by the duality principle applied to Characterization of Meet Irreducible Element.
{{qed}}
Category:Join Irreducible Elements
Category:Join Prime Elements
Category:Distributive Lattices
g37ijkhwugoq1g1y5jiwiqzsew57ki4
Theorem: Velocity with respect to Relative Velocity

Let $A$ and $B$ be bodies in space.
Let $\mathbf v_A$ and $\mathbf v_B$ denote the velocities of $A$ and $B$ such that $\mathbf v_A$ and $\mathbf v_B$ are very much smaller than the speed of light.
Let $\mathbf v_{AB}$ denote the velocity of $A$ relative to $B$.
Then:
:$\mathbf v_A = \mathbf v_{AB} + \mathbf v_B$

Proof:
{{Recall|Relative Velocity|index = 2}}
{{:Definition:Relative Velocity/Definition 2}}
The result follows directly.
{{qed}}
Theorem: Acceleration with respect to Relative Acceleration

Let $A$ and $B$ be bodies in space.
Let $\mathbf a_A$ and $\mathbf a_B$ denote the accelerations of $A$ and $B$.
Let $\mathbf a_{AB}$ denote the acceleration of $A$ relative to $B$.
Then:
:$\mathbf a_A = \mathbf a_{AB} + \mathbf a_B$

Proof:
{{Recall|Relative Acceleration}}
{{:Definition:Relative Acceleration}}
The result follows directly.
{{qed}}
Theorem: Characterization of Meet-Irreducible Open Set

Let $\struct {S, \tau}$ be a topological space.
Let $W \in \tau$.
{{TFAE}}:
:$(1)\quad W$ is a meet-irreducible open set
:$(2)\quad \forall U, V \in \tau : \paren {U \cap V = W \implies U = W \text { or } V = W}$
:$(3)\quad \forall U, V \in \tau : \paren {U \cap V \subseteq W \implies U \subseteq W \text { or } V \subseteq W}$

Proof:
By definition of meet-irreducible open set:
:$W$ is meet-irreducible open set 
{{iff}}:
:$W$ is meet-irreducible in the frame $\struct {\tau, \subseteq}$
By definition of meet-irreducible:
:$W$ is meet-irreducible in the frame $\struct {\tau, \subseteq}$ 
{{iff}}:
:$\forall U, V \in \tau : \paren {U \cap V = W \implies U = W \text { or } V = W}$
From Prime Element iff Meet Irreducible in Distributive Lattice:
:$W$ is meet-irreducible in the frame $\struct {\tau, \subseteq}$ 
{{iff}}:
:$W$ is prime element in the frame $\struct {\tau, \subseteq}$
By definition of prime element:
:$W$ is prime element in the frame $\struct {\tau, \subseteq}$
{{iff}}
:$\forall U, V \in \tau : \paren {U \cap V \subseteq W \implies U \subseteq W \text { or } V \subseteq W}$
The result follows.
{{qed}}
Category:Meet-Irreducible Open Sets
g8hcnobdl8fz9vft855i0r8gajguytt
Theorem: Babczyński Theorem

Let $n$ be a $6$-digit integer of the form $\sqbrk {xyxyxy}$ for digits $x$ and $y$.
Then $n$ is divisible by $3$, $7$, $13$ and $37$.

Proof:
{{begin-eqn}}
{{eqn | l = \sqbrk {xyxyxy}
      | r = \sqbrk {xy} \times 10101
      | c = 
}}
{{eqn | r = \sqbrk {xy} \times 3 \times 7 \times 13 \times 37
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Atom of Countably Generated Sigma-Algebra is Measurable

Let $X$ be a set.
Let $\Sigma$ be a countably generated $\sigma$-algebra of $X$.
Then:
:$\ds \forall x \in X : \quad \sqbrk x_\Sigma \in \Sigma$
where $\sqbrk x_\Sigma$ denotes the atom.

Proof:
By assumption, there is a countable collection $\GG \subseteq \Sigma$ such that:
:$\ds \Sigma = \map \sigma \GG$
Let $x \in X$.
It suffices to show:
:$\ds \sqbrk x_\Sigma = \bigcap_{ x \in A \in \GG } A \cap \bigcap_{ x \not \in A \in \GG} X \setminus A$
$\subseteq$ is clear.
We need to show $\supseteq$.
{{ProofWanted}}
Category:Definitions/Sigma-Algebras
66nbpowxd58t47g3k3yq9d59i4omxx7
Theorem: Join Irreducible Element is Dual of Meet Irreducible Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $z \in S$.
The following are dual statements:
:$z$ is a meet irreducible element of the meet semilattice $\struct {S, \wedge, \preceq}$
:$z$ is a join irreducible element of the join semilattice $\struct {S, \vee, \preceq}$

Proof:
By definition of meet irreducible element:
:$z$ is the meet irreducible element of the meet semilattice $\struct {S, \wedge, \preceq}$
{{iff}}:
:$\forall x, y \in S: \paren{z = x \wedge y} \implies \leftparen{z = x}$ or $\rightparen{z = y}$
By the duality principle, the dual of this statement is:
:$\forall x, y \in S: \paren{z = x \vee y} \implies \leftparen{z = x}$ or $\rightparen{z = y}$
By definition of join irreducible element:
:$z$ is the join irreducible element of the join semilattice $\struct {S, \vee, \preceq}$
{{qed}}
Theorem: Join Prime Element is Dual of Meet Prime Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $z \in S$.
The following are dual statements:
:$z$ is the meet prime element of the meet semilattice $\struct {S, \wedge, \preceq}$
:$z$ is the join prime element of the join semilattice $\struct {S, \vee, \preceq}$

Proof:
By definition of meet prime element:
:$z$ is the meet prime element of the meet semilattice $\struct {S, \wedge, \preceq}$
{{iff}}:
:$\forall x, y \in S: \paren{x \wedge y \preceq z} \implies \leftparen{x \preceq z}$ or $\rightparen{y \preceq z}$
By the duality principle, the dual of this statement is:
:$\forall x, y \in S: \paren{z \preceq x \vee y} \implies \leftparen{z \preceq z}$ or $\rightparen{z \preceq y}$
By definition of join prime element:
:$z$ is the join prime element of the join semilattice $\struct {S, \vee, \preceq}$
{{qed}}
Theorem: Generator of Sigma-Algebra Separates Points

Let $X$ be a set.
Let $\GG \subseteq \powerset X$ be a collection of subsets of $X$.
Let $\map \sigma \GG$ be the $\sigma$-algebra generated by $\GG$.
Let $x, y \in X$.
Suppose that $\map \sigma \GG$ separates $x$ and $y$ in the sense:
:$\exists A \in \map \sigma \GG : \quad  x \in A \quad \wedge \quad y \in X \setminus A$
Then $\GG$ also separates $x$ and $y$ in the sense:
:$\exists A_0 \in \GG : \quad  x \in A_0 \quad \wedge \quad y \in X \setminus A_0$

Proof:
{{AimForCont}}:
:$\forall A_0 \in \GG : \quad  x, y \in A_0 \quad \vee \quad x, y \in X \setminus A_0$
Let:
:$\CC := \set { A \in \map \sigma {\GG} : \quad  x, y \in A \quad \vee \quad x, y \in X \setminus A }$
Then $\CC$ is a $\sigma$-algebra.
Since:
:$\GG \subseteq \CC$
we have:
:$\map \sigma \GG \subseteq \CC$
This means:
:$\forall A \in \map \sigma \GG : \quad  x, y \in A \quad \vee \quad x, y \in X \setminus A$
This is a contradiction.
Hence the result by Proof by Contradiction.
{{qed}}
Category:Definitions/Sigma-Algebras
cya1t0qwy293fo46ehifakgvzykotpy
Theorem: Characterization of Supremum Precedes Element

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$ admit a supremum $a$
Let $b \in S$.
Then:
:$a \preceq b$
{{iff}}:
:$\forall t \in T : t \preceq b$

Proof:
=== Necessary Condition ===
Let $a \preceq b$.
By definition of supremum:
:$a$ is an upper bound for $T$
By definition of upper bound:
:$\forall t \in T : t \preceq a$
From {{Ordering-axiom|2}}:
:$\forall t \in T : t \preceq b$
{{qed|lemma}}
Theorem: Integral of Integrable Function is Additive/Complex Function

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\struct {\C, \map \BB \C}$ be the complex numbers made into a measurable space with its Borel $\sigma$-algebra.
Let $f, g : X \to \C$ be a $\mu$-integrable function.
Then $f + g$ is $\mu$-integrable and:
:$\ds \int \paren {f + g} \rd \mu = \int f \rd \mu + \int g \rd \mu$

Proof:
From Addition of Real and Imaginary Parts, we have:
:$\map \Re {f + g} = \map \Re f + \map \Re g$
and:
:$\map \Im {f + g} = \map \Im f + \map \Im g$
Since $f$ is $\mu$-integrable:
:$\map \Re f$ and $\map \Im f$ are $\mu$-integrable.
Similarly since $g$ is $\mu$-integrable:
:$\map \Re g$ and $\map \Im g$ are $\mu$-integrable.
From Integral of Integrable Function is Additive, we have:
:$\map \Re f + \map \Re g = \map \Re {f + g}$ is $\mu$-integrable
with:
:$\ds \int \map \Re {f + g} \rd \mu = \int \map \Re f \rd \mu + \int \map \Re g \rd \mu$ 
Also from Integral of Integrable Function is Additive, we have:
:$\map \Im f + \map \Im g = \map \Im {f + g}$ is $\mu$-integrable
with:
:$\ds \int \map \Im {f + g} \rd \mu = \int \map \Im f \rd \mu + \int \map \Im g \rd \mu$ 
Hence $f + g$ is $\mu$-integrable.
Further, we have:
{{begin-eqn}}
{{eqn	| l = \int \paren {f + g} \rd \mu
		| r = \int \map \Re {f + g} \rd \mu + i \int \map \Im {f + g} \rd \mu 
		| c = {{Defof|Integral of Complex Measure-Integrable Function}}
}}
{{eqn	| r = \paren {\int \map \Re f \rd \mu + \int \map \Re g \rd \mu} + i \paren {\int \map \Im f \rd \mu + \int \map \Im g \rd \mu} 
}}
{{eqn	| r = \paren {\int \map \Re f \rd \mu + i \int \map \Im f \rd \mu} + \paren {\int \map \Re g \rd \mu + i \int \map \Im g \rd \mu} 
}}
{{eqn	| r = \int f \rd \mu + \int g \rd \mu 
}}
{{end-eqn}}
{{qed}}
Category:Integral of Integrable Function is Additive
Category:Complex Measure-Integrable Functions
ecfur7uoan36zskeih7bo91nu7sfcqh
Theorem: Integral of Integrable Function is Homogeneous/Complex Function

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\struct {\C, \map \BB \C}$ be the complex numbers made into a measurable space with its Borel $\sigma$-algebra.
Let $f : X \to \C$ be a $\mu$-integrable function.
Let $\lambda \in \C$. 
Then $\lambda f$ is $\mu$-integrable and:
:$\ds \int \lambda f \rd \mu = \lambda \int f \rd \mu$

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \lambda \int f \rd \mu
		| r = \paren {\map \Re \lambda + i \Im \lambda} \int \map \Re f \rd \mu + i \paren {\map \Re \lambda + i \map \Im \lambda} \int \Im f \rd \mu 
}}
{{eqn	| r = \paren {\map \Re \lambda \int \map \Re f \rd \mu - \map \Im \lambda \int \map \Im f \rd \mu} + i \paren {\map \Im \lambda \int \map \Re f \rd \mu + \map \Re \lambda \int \map \Im f \rd \mu}
}}
{{end-eqn}}
From Real Part of Complex Product, we have:
:$\map \Re {\lambda f} = \map \Re \lambda \map \Re f - \map \Im \lambda \map \Im f$
From Imaginary Part of Complex Product, we have:
:$\map \Im {\lambda f} = \map \Im \lambda \map \Re f + \map \Re \lambda \map \Im f$
Since $f$ is $\mu$-integrable, $\map \Re f$ and $\map \Im f$ are $\mu$-integrable by definition.
From Integral of Integrable Function is Additive and Integral of Integrable Function is Homogeneous, $\map \Re {\lambda f}$ and $\map \Im {\lambda f}$ are both $\mu$-integrable and we have:
:$\ds \int \map \Re {\lambda f} \rd \mu = \map \Re \lambda \int \map \Re f \rd \mu - \map \Im \lambda \int \map \Im f \rd \mu$
and:
:$\ds \int \map \Im {\lambda f} \rd \mu = \map \Im \lambda \int \map \Re f \rd \mu + \map \Re \lambda \int \map \Im f \rd \mu$
Then $\lambda f$ is $\mu$-integrable.
We then have:
{{begin-eqn}}
{{eqn	| l = \int \lambda f \rd \mu
		| r = \paren {\map \Re \lambda \int \map \Re f \rd \mu - \map \Im \lambda \int \map \Im f \rd \mu} + i \paren {\map \Im \lambda \int \map \Re f \rd \mu + \map \Re \lambda \int \map \Im f \rd \mu}
}}
{{eqn	| r = \lambda \int f \rd \mu 
}}
{{end-eqn}}
{{qed}}
Category:Integral of Integrable Function is Homogeneous
bhtm7rkrf5badn4iikrovekzgkxvw02
Theorem: Complex Modulus of Measurable Function is Measurable

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\struct {\C, \map \BB \C}$ be the complex numbers made into a measurable space with its Borel $\sigma$-algebra.
Let $f : X \to \C$ be a $\Sigma/\map \BB \C$-measurable mapping.
Let $\struct {\R, \map \BB \R}$ be the real numbers made into a measurable space with its Borel $\sigma$-algebra.
Then $\cmod f : X \to \R$ is $\Sigma/\map \BB \R$-measurable.

Proof:
From Complex Modulus Function is Continuous, the mapping $\cmod {\, \cdot \,} : \C \to \R$ is continuous.
From Continuous Mapping is Measurable, $\cmod {\, \cdot \,} : \C \to \R$ is $\map \BB C/\map \BB \R$-measurable.
Hence from Composition of Measurable Mappings is Measurable, $\cmod f : X \to \R$ is $\Sigma/\map \BB \R$-measurable.
{{qed}}
Category:Measurable Functions
rjbk2918n4d30gddqa2m1fwj3m4cenw
Theorem: Existence of Smooth Transition Function in One Dimension/Lemma

$f$ is smooth with:
:$\ds \map {f^{(n)} } x = \begin{cases}\map {P_n} {\frac 1 x} e^{-1/x} & x > 0 \\ 0 & x \le 0\end{cases}$
for each $n \ge 1$, for some polynomial $P_n$.

Proof:
We proceed by Proof by Mathematical Induction.
For $n \ge 1$, let $\map Q n$ be the proposition:
:$f$ is $n$ times differentiable and there exists a polynomial $P_n$ with positive leading coefficient such that:
::$\ds \map {f^{(n)} } x = \begin{cases}\map {P_n} {\frac 1 x} e^{-1/x} & x > 0 \\ 0 & x \le 0\end{cases}$
Theorem: Existence of Smooth Transition Function in One Dimension

Let $a, b, c, d \in \R$ be real numbers with $a < b < c < d$. 
Then there exists a smooth function $h : \R \to \closedint 0 1$ such that:
:$\map h x = 1$ for $x \in \closedint b c$
and:
:$\map h x = 0$ for $x \in \R \setminus \openint a d$

Proof:
First define $f : \R \to \R$ by:
:$\ds \map f x = \begin{cases}e^{-1/x} & x \ge 0 \\ 0 & x < 0\end{cases}$
for each $x \in \R$.
Note that $\map f x \ge 0$ for all $x \in \R$. 
We first show that $f$ is smooth.
Theorem: Limit of Countable Union of Unbounded Below Closed Intervals

Let $x \in \R$. 
,
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence converging to $x$ such that $x_n < x$ for each $n \in \N$.
Then we have:
:$\ds \bigcup_{n \mathop = 1}^\infty \hointl {-\infty} {x_n} = \openint {-\infty} x$

Proof:
First suppose that:
:$\ds t \in \bigcup_{n \mathop = 1}^\infty \hointl {-\infty} {x_n}$
Then we have:
:$t \le x_n$ for some $n \in \N$.
We have $x_n < x$ for each $n \in \N$.
Hence $t < x$ and $t \in \openint {-\infty} x$.
Now suppose that $t \in \openint {-\infty} x$.
Then $t < x$. 
Hence we can take $\epsilon > 0$ such that:
:$t + \epsilon < x$
so that:
:$t < x - \epsilon$ 
Since $x_n \to x$, there exists $N \in \N$ such that:
:$x - \epsilon \le x_n \le x + \epsilon$ for $n \ge N$. 
Hence we have:
:$t \le x_N$ 
In particular, $t \in \openinl {-\infty} {x_N}$, so:
:$\ds t \in \bigcup_{n \mathop = 1}^\infty \openinl {-\infty} {x_n}$ 
So we have:
:$\ds \openint {-\infty} x \subseteq \bigcup_{n \mathop = 1}^\infty \hointl {-\infty} {x_n}$
{{qed}}
Category:Limits of Sequences of Intervals
jpq6uwi7r015sf0tafenid28v33tp87
Theorem: Monotonic Sequence Characterization of Left Limit of Function

Let $\hointl a b$ be a real interval. 
Let $x \in \hointl a b$. 
Let $f : \hointl a b \to \R$ be a real function.
Let $L \in \R$. 
Then:
:$\ds \lim_{y \mathop \to x^-} \map f y = L$ 
{{iff}}:
:for all monotone sequences $\sequence {x_n}_{n \mathop \in \N}$, with $x_n < x$ for each $n$, that converge to $x$ we have:
::$\map f {x_n} \to L$

Proof:
=== Necessary Condition ===
Suppose that:
:$\ds \lim_{y \to x^-} \map f y = L$
then:
:for each real sequence $\sequence {x_n}_{n \mathop \in \N}$, with $x_n < x$ for each $n$, converging to $x$ we have:
::$\map f {x_n} \to L$
from Limit of Function by Convergent Sequences: Corollary.
So in particular: 
:for all monotone sequences $\sequence {x_n}_{n \mathop \in \N}$, with $x_n < x$ for each $n$, that converge to $x$ we have:
::$\map f {x_n} \to L$
{{qed|lemma}}
Theorem: Left Limit of Distribution Function of Finite Borel Measure

Let $\mu$ be a finite Borel measure.
Let $F_\mu$ be the distribution function of $\mu$.
Then we have:
:$\ds \lim_{y \mathop \to x^-} \map {F_\mu} y = \map \mu {\openint {-\infty} x}$

Proof:
From Monotonic Sequence Characterization of Left Limit of Function, the claim is equivalent to:
:for all monotone sequences $\sequence {x_n}_{n \mathop \in \N}$, with $x_n < x$ for each $n$, that converge to $x$ we have:
::$\map {F_\mu} {x_n} \to \map \mu {\openint {-\infty} x}$
That is:
:$\map \mu {\hointl {-\infty} {x_n} } \to \map \mu {\openint {-\infty} x}$
Let $\sequence {x_n}_{n \mathop \in \N}$ be a monotone sequence with $x_n < x$ for each $n \in \N$, satisfying $x_n \to x$. 
From Limit of Countable Union of Unbounded Below Closed Intervals, we have:
:$\hointl {-\infty} {x_n} \uparrow \openint {-\infty} x$
where $\uparrow$ denotes the limit of an increasing sequence of sets.
From Measure of Limit of Increasing Sequence of Measurable Sets, we therefore have:
:$\map \mu {\hointl {-\infty} {x_n} } \to \map \mu {\openint {-\infty} x}$
Invoking Monotonic Sequence Characterization of Left Limit of Function, we obtain:
:$\ds \lim_{y \mathop \to x^-} \map {F_\mu} y = \map \mu {\openint {-\infty} x}$
{{qed}}
Category:Distribution Function of Finite Borel Measure
fzpewnk80l36ld6wtk3mbbqwm3ecsli
Theorem: Distribution Function of Finite Borel Measure is Continuous at Point iff Measure Continuous at Point

Let $\mu$ be a finite Borel measure.
Let $F_\mu$ be the distribution function of $\mu$.
Let $x \in \R$.
Then $F_\mu$ is continuous at $x$ {{iff}} $\map \mu {\set x} = 0$.

Proof:
From Distribution Function of Finite Borel Measure is Right-Continuous, $F_\mu$ is right-continuous at $x$.
Hence from Continuous at Point iff Left-Continuous and Right-Continuous, the claim is equivalent to:
:$F_\mu$ is left-continuous at $x$ {{iff}} $\map \mu {\set x} = 0$.
That is:
:$\ds \lim_{y \to x^-} \map {F_\mu} y = \map {F_\mu} x$
{{iff}}:
:$\map \mu {\set x} = 0$ 
From Left Limit of Distribution Function of Finite Borel Measure, this is equivalent to:
:$\map \mu {\hointl {-\infty} x} = \map \mu {\openint {-\infty} x}$ {{iff}} $\map \mu {\set x} = 0$.
From Measure of Set Difference with Subset, we indeed have that:
:$\map \mu {\hointl {-\infty} x} = \map \mu {\openint {-\infty} x}$ {{iff}} $\map \mu {\hointl {-\infty} x} - \map \mu {\openint {-\infty} x} = \map \mu {\set x} = 0$
as required.
{{qed}}
Category:Distribution Function of Finite Borel Measure
fg2jwditadbv136x9pzz00w9mwejvwk