avewright/proofwiki-math huggingface dataset:
Theorem: Dilation of Closed Unit Ball in Normed Vector Space Decomposes as Sum of Dilations

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a normed vector space over $\GF$.
Let $\lambda, \mu > 0$.
Let $B_X^-$ be the closed unit ball in $\struct {X, \norm {\, \cdot \,}_X}$.
Then:
:$\paren {\lambda + \mu} B_X^- = \lambda B_X^- + \mu B_X^-$

Proof:
Let $y \in \paren {\lambda + \mu} B_X^-$.
Then there exists $x \in B_X^-$ such that $y = \paren {\lambda + \mu} x$.
Write:
:$y = \lambda x + \mu x \in \lambda B_X^- + \mu B_X^-$
We therefore have that $\paren {\lambda + \mu} B_X^- \subseteq \lambda B_X^- + \mu B_X^-$. 
Now let $y \in \lambda B_X^- + \mu B_X^-$.
Hence there exists $u, v \in B_X^-$ such that $y = \lambda u + \mu v$. 
Then we have:
{{begin-eqn}}
{{eqn	| l = \norm y_X
		| r = \norm {\lambda u + \mu v}_X
}}
{{eqn	| o = \le
		| r = \norm {\lambda u}_X + \norm {\mu v}_X 
		| c = {{NormAxiomVector|3}}
}}
{{eqn	| r = \lambda \norm u_X + \mu \norm v_X 
}}
{{eqn	| o = \le 
		| r = \lambda + \mu 
		| c = since $\norm u_X \le 1$ and $\norm v_X \le 1$ 
}}
{{end-eqn}}
Hence:
:$\ds \norm {\frac y {\lambda + \mu} }_X \le 1$
Hence $y \in \paren {\lambda + \mu} B_X^-$.
Hence we have:
:$\lambda B_X^- + \mu B_X^- \subseteq \paren {\lambda + \mu} B_X^-$
We conclude:
:$\paren {\lambda + \mu} B_X^- = \lambda B_X^- + \mu B_X^-$
{{qed}}
Category:Normed Vector Spaces
mihmnvv6qvloko0ut82rtaj4b8nn7c7
Theorem: Linear First Order ODE/y' - y = 3

The linear first order ODE:
:$(1): \quad \dfrac {\d y} {\d x} - y = 3$
has the general solution:
:$y = C e^x - 3$

Proof:
$(1)$ is a linear first order ODE in the form:
:$\dfrac {\d y} {\d x} + \map P x y = \map Q x$
where:
:$\map P x = -1$
:$\map Q x = 3$
Thus:
{{begin-eqn}}
{{eqn | l = \int \map P x \rd x
      | r = -\int \rd x
      | c = 
}}
{{eqn | r = -x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{\int P \rd x}
      | r = e^{-x}
      | c = 
}}
{{end-eqn}}
Thus from Solution by Integrating Factor, $(1)$ can be rewritten as:
{{begin-eqn}}
{{eqn | l = \map {\dfrac {\d} {\d x} } {y e^{-x} }
      | r = 3 e^{-x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y e^{-x}
      | r = \int 3 e^{-x} \rd x
      | c = 
}}
{{eqn | r = 3 \frac {e^{-x} } {-1} + C
      | c = Primitive of $e^{a x}$ for $a = -1$
}}
{{eqn | r = -3 e^{-x} + C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = C e^x - 3
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: One-Sided Prepolar Reverses Subset Relation

Let $\innerprod E F$ be a dual system over $\R$.
Let $B, C \subseteq F$ be non-empty such that $B \subseteq C$. 
Let $B_\odot$ and $C_\odot$ be the one-sided prepolars of $B$ and $C$ respectively.
Then:
:$C_\odot \subseteq B_\odot$

Proof:
Let $x \in C_\odot$.
Then we have:
:$\innerprod x f \le 1$ for all $f \in C$.
Since $f \in B$, we in particular have:
:$\innerprod x f \le 1$ for all $f \in B$.
Hence $x \in B_\odot$.
Hence $C_\odot \subseteq B_\odot$.
{{qed}}
Category:One-Sided Prepolars
kit9bf2tot7bcx9j6eguyz761ecamp0
Theorem: One-Sided Prepolar of Dilation

Let $\innerprod E F$ be a dual system over $\R$.
Let $B \subseteq F$ be non-empty.
Let $\lambda > 0$. 
Let $B_\odot$ and $\paren {\lambda B}_\odot$ be the one-sided polar of $B$ and $B_\odot`$ respectively.
Then:
:$\paren {\lambda B}_\odot = \dfrac 1 \lambda B_\odot$

Proof:
Let $x \in \dfrac 1 \lambda B_\odot$. 
This is the case {{iff}} $\lambda x \in B_\odot$.
This is equivalent to $\innerprod {\lambda x} f \le 1$ for each $f \in B$.
Since $\innerprod \cdot \cdot$ is bilinear, we have $\innerprod {\lambda x} f = \innerprod x {\lambda f}$.
Hence $\innerprod x {\lambda f} \le 1$ for each $x \in A$ is equivalent to $\innerprod x {\lambda f} \le 1$ for each $f \in B$.
This is equivalent to $\innerprod x g \le 1$ for each $g \in \lambda B$.
This is equivalent to $x \in \paren {\lambda B}_\odot$.
Hence:
:$\paren {\lambda B}_\odot = \dfrac 1 \lambda B_\odot$ 
{{qed}}
Category:One-Sided Prepolars
qp3v1anpbf6nic0zeotsijdmtfaba6w
Theorem: Linear Second Order ODE/y'' + k^2 y = 0/y(0) = 2, y'(0) = 1

The second order ODE:
:$(1): \quad y' ' + k^2 y = 0$
with initial conditions:
:$\map y 0 = 2$
:$\map {y'} 0 = 1$
has the particular solution:
:$y = 2 \cos k x + \dfrac {\sin k x} k$

Proof:
From Linear Second Order ODE: $y' ' + k^2 y = 0$, the general solution of $(1)$ is:
:$y = C_1 \sin k x + C_2 \cos k x$
Differentiating {{WRT|Differentiation}} $x$:
:$y' = k C_1 \cos k x - k C_2 \sin k x$
Thus for the initial conditions:
{{begin-eqn}}
{{eqn | l = \map y 0
      | r = C_1 \sin 0 + C_2 \cos 0
      | c = 
}}
{{eqn | r = 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = C_2
      | r = 2
      | c = as $\sin 0 = 0$ and $\cos 0 = 1$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map {y'} 0
      | r = k C_1 \cos 0 - k C_2 \sin 0
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = k C_1
      | r = 1
      | c = as $\sin 0 = 0$ and $\cos 0 = 1$
}}
{{eqn | ll= \leadsto
      | l = C_1
      | r = \dfrac 1 k
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Proper Convex Combination of Interior of Convex Set and Closure of Convex Set is Contained in Interior of Set

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \tau}$ be a topological vector space over $\GF$.
Let $C \subseteq X$ be a convex set with non-empty interior $\Int C$. 
Let $\map \cl C$ be the closure of $C$ in $\struct {X, \tau}$.
Let $t \in \openint 0 1$. 
Then we have:
:$t \Int C + \paren {1 - t} \map \cl C \subseteq \Int C$

Proof:
Let $x \in \Int C$ and $y \in \map \cl C$ so that $t x + \paren {1 - t} y \in t \Int C + \paren {1 - t} \map \cl C$ is general.
From Classification of Open Neighborhoods in Topological Vector Space, there exists an open neighborhood of ${\mathbf 0}_X$ in $\struct {X, \tau}$ such that $x + U \subseteq \Int C$.
From Dilation of Open Set in Topological Vector Space is Open:
:$\ds -\frac t {1 - t} U$ is an open neighborhood of ${\mathbf 0}_X$ in $\struct {X, \tau}$.
From Translation of Open Set in Topological Vector Space is Open:
:$\ds y - \frac t {1 - t} U$ is an open neighborhood of $y$ in $\struct {X, \tau}$.
Since $y \in \map \cl C$, we have:
:$\ds C \cap \paren {y - \frac t {1 - t} U} \ne \O$
Take:
:$\ds z \in C \cap \paren {y - \frac t {1 - t} U}$
Hence:
:$\ds z \in y - \frac t {1 - t} U$
Hence:
:$\ds y - z \in \frac t {1 - t} U$
so that:
:$\paren {1 - t} \paren {y - z} \in t U$
Since $x + U \subseteq \Int C \subseteq C$ and $z \in C$, we have:
:$V = t \paren {x + U} + \paren {1 - t} z \subseteq C$ 
From Dilation of Open Set in Topological Vector Space is Open and Translation of Open Set in Topological Vector Space is Open, $V$ is open.
Further, we write:
:$t x + \paren {1 - t} y = t x + \paren {1 - t} \paren {y - z} + \paren {1 - t} z$
Since $\paren {1 - t} \paren {y - z} \in t U$, we have $t x + \paren {1 - t} \paren {y - z} \in t x + t U = t \paren {x + U}$
Hence we have:
:$t x + \paren {1 - t} y \in t \paren {x + U} + \paren {1 - t} z = V$
Since $V \subseteq C$ is open, we have:
:$t x + \paren {1 - t} y \in \Int C$
Hence:
:$t \Int C + \paren {1 - t} \map \cl C \subseteq \Int C$
{{qed}}
Theorem: Closure of Convex Set in Topological Vector Space with Non-Empty Interior coincides with Closure of Interior

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \tau}$ be a topological vector space over $\GF$.
Let $C \subseteq X$ be a convex set with non-empty interior $\Int C$. 
Let $\cl$ be the closure taken in $\struct {X, \tau}$.
Then:
:$\map \cl C = \map \cl {\Int C}$

Proof:
Firstly, from Topological Closure of Subset is Subset of Topological Closure, we have:
:$\map \cl {\Int C} \subseteq \map \cl C$
Conversely, take $x \in \map \cl C$.
Fix $z \in \Int C$. 
From Proper Convex Combination of Interior of Convex Set and Closure of Convex Set is Contained in Interior of Set, we have:
:$\ds \frac 1 n \Int C + \paren {1 - \frac 1 n} \map \cl C \subseteq \Int C$
We therefore have:
:$\ds \frac 1 n z + \paren {1 - \frac 1 n} x \in \Int C$ for each $n \in \N$. 
From Multiple of Vector in Topological Vector Space Converges, we have:
:$\ds \frac 1 n z + \paren {1 - \frac 1 n} = \frac 1 n \paren {z - x} + x \to x$ as $n \to \infty$. 
Hence from Point in Set Closure iff Limit of Net we have that $x \in \map \cl {\Int C}$.
Hence we have $\map \cl C \subseteq \map \cl {\Int C}$.
We conclude that $\map \cl C = \map \cl {\Int C}$.
{{qed}}
Theorem: Open Neighborhood of Origin in Topological Vector Space is Absorbing

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \tau}$ be a topological vector space over $\GF$.
Let $U$ be an open neighborhood of ${\mathbf 0}_X$ in $\struct {X, \tau}$.
Then $U$ is absorbing.

Proof:
Define $m : \GF \times X \to X$ by:
:$\map m {\lambda, x} \mapsto \lambda x$
for any $\tuple {\lambda, x} \in \GF \times X$.
From the definition of a topological vector space, the mapping $f$ is continuous.
From Vertical Section of Continuous Function is Continuous, the mapping $m_x : \GF \to X$ defined by:
:$\map {m_x} \lambda = \lambda x$ 
for each $\lambda \in \GF$, is continuous.
Hence there exists $\delta > 0$ such that $\cmod \lambda < \delta$ implies that $\lambda x \in U$.
That is, $x \in \lambda^{-1} U$ for $\cmod \lambda < \delta$. 
We have $0 < \cmod {\lambda} < \delta$ {{iff}} $\cmod {\lambda^{-1} } > \delta^{-1}$.
Hence we have $x \in \mu U$ for $\cmod \mu > \delta^{-1}$. 
Hence $U$ is absorbing.
{{qed}}
Category:Topological Vector Spaces
Category:Absorbing Sets
98vo0cum8y74x02dvc7eqc9ocj6s38k
Theorem: Interior of Closure of Convex Set in Topological Vector Space with Non-Empty Interior coincides with Interior of Set

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \tau}$ be a topological vector space over $\GF$.
Let $C \subseteq X$ be a convex set with non-empty interior $\Int C$. 
Let $\cl$ be the closure taken in $\struct {X, \tau}$.
Then we have:
:$\Int {\map \cl C} = \Int C$

Proof:
From Interior of Subset, we have $\Int C \subseteq \Int {\map \cl C}$.
We aim to show that $\Int {\map \cl C} \subseteq \Int C$. 
Let $x \in \Int {\map \cl C}$. 
Fix $x_0 \in \Int C$. 
From Classification of Open Neighborhoods in Topological Vector Space, there exists an open neighborhood $W$ of ${\mathbf 0}_X$ in $\struct {X, \tau}$ such that $x + W \subseteq \map \cl C$.
From Open Neighborhood of Origin in Topological Vector Space is Absorbing, $W$ is absorbing.
Hence there exists $n \in \N$ such that:
:$\ds x - x_0 \in n W$
Then:
:$\ds \frac 1 n \paren {x - x_0} \in W$
Let $\epsilon = 1/n$. 
Then we have $x + \epsilon \paren {x - x_0} \in x + W \subseteq \map \cl C$.
From Proper Convex Combination of Interior of Convex Set and Closure of Convex Set is Contained in Interior of Set, we have:
:$\ds \epsilon \Int C + \paren {1 - \epsilon} \map \cl C \subseteq \Int C$
Hence we have:
:$\epsilon x_0 + \paren {1 - \epsilon} x \in \Int C$
since $x_0 \in \Int C \subseteq C$ and $x \in \Int {\map \cl C} \subseteq \map \cl C$.
We can rewrite this as:
:$x - \epsilon \paren {x - x_0} \in \Int C$ 
Hence:
:$x + \epsilon \paren {x - x_0} \in \map \cl C$
and:
:$x - \epsilon \paren {x - x_0} \in \Int C$
From Proper Convex Combination of Interior of Convex Set and Closure of Convex Set is Contained in Interior of Set, we have:
:$\ds \frac 1 2 \Int C + \frac 1 2 \map \cl C \subseteq \Int C$
Hence:
:$\ds x = \frac 1 2 \paren {x + \epsilon \paren {x - x_0} } + \frac 1 2 \paren {x - \epsilon \paren {x - x_0} } \in \Int C$ 
Hence $\Int {\map \cl C} \subseteq \Int C$.
Hence $\Int {\map \cl C} = \Int C$.
{{qed}}
Theorem: Bound on Difference of Values of Convex Real Function

Let $X$ be a vector space over $\R$.
Let $C \subseteq X$ be a convex set.
Let $f : C \to \R$ be a convex function.
Let $x \in C$.
Let $z \in C$ be such that:
:$x + z \in C$ and $x - z \in C$.
Let $\delta \in \closedint 0 1$.
Then $x + \delta z \in C$, $x - \delta z \in C$, and further:
:$\cmod {\map f {x + \delta z} - \map f x} \le \delta \max \set {\map f {x + z} - \map f x, \map f {x - z} - \map f x}$

Proof:
Write:
:$x + \delta z = \paren {1 - \delta} x + \delta \paren {x + z}$ 
and:
:$x - \delta z = \paren {1 - \delta} x + \delta \paren {x - z}$
Since $C$ is convex, we have $x + \delta z \in C$ and $x - \delta z \in C$.
Since $f$ is convex, we then have:
:$\map f {x + \delta z} \le \paren {1 - \delta} \map f x + \delta \map f {x + z}$
and:
:$\map f {x - \delta z} \le \paren {1 - \delta} \map f x + \delta \map f {x - z}$ 
Rearranging, we have:
:$\map f {x + \delta z} - \map f x \le \delta \paren {\map f {x + z} - \map f x}$
and:
:$\map f {x - \delta z} - \map f x \le \delta \paren {\map f {x - z} - \map f x}$
Now, write:
:$\ds x = \frac 1 2 \paren {x + \delta z} + \frac 1 2 \paren {x - \delta z}$
Since $f$ is convex, we then have:
:$\ds \map f x \le \frac 1 2 \map f {x + \delta z} + \frac 1 2 \map f {x - \delta z}$
Multiplying by $2$ we have:
:$\map f x + \map f x \le \map f {x + \delta z} + \map f {x - \delta z}$
and hence:
:$\map f x - \map f {x + \delta z} \le \map f {x - \delta z} - \map f x$ 
We have already established that:
:$\map f {x - \delta z} - \map f x \le \delta \paren {\map f {x - z} - \map f x}$
so we have:
:$\map f x - \map f {x + \delta z} \le \delta \paren {\map f {x - z} - \map f x}$ 
So we have:
:$\map f {x + \delta z} - \map f x \le \delta \paren {\map f {x + z} - \map f x} \le \delta \max \set {\map f {x + z} - \map f x, \map f {x - z} - \map f x}$
and:
:$\map f x - \map f {x + \delta z} \le \delta \paren {\map f {x - z} - \map f x} \le \delta \max \set {\map f {x + z} - \map f x, \map f {x - z} - \map f x}$
Hence we have:
:$\cmod {\map f {x + \delta z} - \map f x} \le \delta \max \set {\map f {x + z} - \map f x, \map f {x - z} - \map f x}$ 
{{qed}}
Theorem: Local Criterion for Continuity of Convex Real Function

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \tau}$ be a topological vector space over $\GF$.
Let $C \subseteq X$ be a convex set with non-empty interior $\Int C$.
Let $x \in \Int C$.
Let $U$ be an open neighborhood of $x$ in $\Int C$. 
Let $f : C \to \R$ be a convex real function such that:
:$\ds \sup_{z \mathop \in U} \map f z < \infty$
Then $f$ is continuous at $x$.

Proof:
From Classification of Open Neighborhoods in Topological Vector Space, there exists an open neighborhood $V$ of ${\mathbf 0}_X$ such that:
:$U = x + V$
From Open Neighborhood of Point in Topological Vector Space contains Sum of Open Neighborhoods: Corollary 2, we can take $V$ to be balanced by passing to a subset.
In particular, from Balanced Set in Vector Space is Symmetric, $V$ is symmetric. 
Then for each $z \in V$, we have $x + z \in x + V$ and $x - z \in x + V$. 
Take:
:$\ds M > \max \set {0, -\map f x + \sup_{z \mathop \in U} \map f z}$ 
so that:
:$\map f y < \map f x + M$ for all $y \in x + V$.
Then:
:$\map f {x + z} < \map f x + M$
and:
:$\map f {x - z} < \map f x + M$
so that:
:$\max \set {\map f {x + z} - \map f x, \map f {x - z} - \map f x} < M$
Let $\epsilon > 0$.
Take $\delta \in \openint 0 1$ such that $\delta M < \epsilon$.
From Bound on Difference of Values of Convex Real Function, we have:
:$\cmod {\map f {x + \delta z} - \map f x} \le \delta \max \set {\map f {x + z} - \map f x, \map f {x - z} - \map f x}$ for each $z \in V$.
Hence:
:$\cmod {\map f {x + \delta z} - \map f x} < \delta M < \epsilon$
Hence we have:
:$\cmod {\map f y - \map f x} < \epsilon$ for all $y \in x + \delta V$.
From Translation of Open Set in Topological Vector Space is Open and Dilation of Open Set in Topological Vector Space is Open, we have that $x + \delta V$ is an  open neighborhood of $x$ satisfying $f \sqbrk {x + \delta V} \subseteq \openint {\map f x - \epsilon} {\map f x + \epsilon}$. 
Since $\epsilon > 0$ was arbitrary, $f$ is continuous at $x$.
{{qed}}
Theorem: Lower Limit of Function is Bounded Above by Value at Limit Point

Let $\struct {X, \tau}$ be a topological space.
Let $f : X \to \overline \R$ be a function.
Let $\liminf$ be the lower limit.
Let $x_0 \in X$.
Then we have:
:$\ds \liminf_{x \mathop \to x_0} \map f x \le \map f {x_0}$

Proof:
Let $\map \mho {x_0}$ be the set of open neighborhoods of $x_0$ in $\struct {X, \tau}$.
Then for each $V \in \map \mho {x_0}$, we have:
:$\ds \inf_{x \mathop \in V} \map f x \le \map f {x_0}$
since $x_0 \in V$. 
Hence:
:$\ds \sup_{V \in \map \mho {x_0} } \paren {\inf_{x \mathop \in V} \map f x} \le \map f {x_0}$ 
Hence by the definition of the lower limit, we have:
:$\ds \liminf_{x \mathop \to x_0} \map f x \le \map f {x_0}$
{{qed}}
Category:Limits of Mappings
Category:Lower Limit of Function is Bounded Above by Value at Limit Point
0uv9jrpjh7wd630al5tcmss3f45gl8z
Theorem: Negative of Lower Limit is Upper Limit

Let $\struct {S, \tau}$ be a topological space.
Let $f : S \to \overline \R$ be an extended real valued function.
Let $x_0 \in S$.
Then:
:$\ds \limsup_{x \mathop \to x_0} \map f x = -\liminf_{x \mathop \to x_0} \paren {-\map f x}$
where $\limsup$ is the upper limit and $\liminf$ is the lower limit.

Proof:
Let $\map \mho {x_0}$ be the set of open neighborhoods of $x_0$ in $\struct {X, \tau}$.
We then have:
{{begin-eqn}}
{{eqn	| l = -\liminf_{x \mathop \to x_0} \paren {-\map f x}
		| r = -\sup_{V \in \map \mho {x_0} } \paren {\inf_{x \mathop \in V} \paren {-\map f x} }
		| c = {{Defof|Lower Limit (Topological Space)}}
}}
{{eqn	| r = \inf_{V \in \map \mho {x_0} } \paren {-\inf_{x \mathop \in V} \paren {-\map f x} }
		| c = Negative of Supremum is Infimum of Negatives
}}
{{eqn	| r = \inf_{V \in \map \mho {x_0} } \paren {\sup_{x \mathop \in V} \map f x}
		| c = Negative of Infimum is Supremum of Negatives
}}
{{eqn	| r = \limsup_{x \mathop \to x_0} \map f x
		| c = {{Defof|Upper Limit (Topological Space)}}
}}
{{end-eqn}}
{{qed}}
Category:Lower Limits (Topological Spaces)
Category:Upper Limits (Topological Spaces)
154wnnntew2pk6ls7hp6190a1kecnvw
Theorem: Function is Upper Semicontinuous iff Negative is Lower Semicontinuous

Let $\struct {S, \tau}$ be a topological space.
Let $f : S \to \overline \R$ be an extended real valued function.
Let $x_0 \in S$.
Then $f$ is upper semicontinuous at $x_0$ {{iff}} $-f$ is lower semicontinuous at $x_0$.

Proof:
We have that $f$ is upper semicontinuous at $x_0$ {{iff}}:
:$\ds \map f {x_0} = \limsup_{x \mathop \to x_0} \map f x$
where $\limsup$ is the upper limit.
This is equivalent to:
:$\ds -\map f {x_0} = -\limsup_{x \mathop \to x_0} \map f x$
From Negative of Lower Limit is Upper Limit, we have:
:$\ds -\limsup_{x \mathop \to x_0} \map f x = \liminf_{x \mathop \to x_0} \paren {-\map f x}$
where $\liminf$ is the lower limit.
Hence:
:$\ds \map f {x_0} = \limsup_{x \mathop \to x_0} \map f x$
{{iff}}:
:$\ds -\map f {x_0} = \liminf_{x \mathop \to x_0} \paren {-\map f x}$
Hence $f$ is upper semicontinuous at $x_0$ {{iff}} $-f$ is lower semicontinuous at $x_0$. 
{{qed}}
Category:Upper Semicontinuity
Category:Lower Semicontinuity
31bh0i1xarjnjakmiwxqt3mthpf2gs1
Theorem: Characterization of Upper Semicontinuity

Let $\struct {S, \tau}$ be a topological space.
Let $f: S \to \overline \R$ be an extended real valued function.
{{TFAE}}
:$(1): \quad$ $f$ is upper semicontinuous
:$(2): \quad$ $\set {x \in S : \map f x \ge \alpha}$ is closed for each $\alpha \in \R$
:$(3): \quad$ the hypograph $\map {\operatorname {hypo} } f$ is closed in $S \times \R$.

Proof:
=== $(1)$ implies $(2)$ ===
Suppose that $f$ is upper semicontinuous.
From Function is Upper Semicontinuous iff Negative is Lower Semicontinuous, $-f$ is lower semicontinuous.
From Characterization of Lower Semicontinuity, we have that:
:$\set {x \in S : -\map f x \le -\alpha}$ is closed for each $\alpha \in \R$.
Hence:
:$\set {x \in S : \map f x \ge \alpha}$ is closed for each $\alpha \in \R$.
{{qed|lemma}}
Theorem: Global Criterion for Continuity of Convex Real Function

Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \tau}$ be a topological vector space over $\GF$.
Let $C \subseteq X$ be an open convex set.
Let $f : C \to \R$ be a convex function.
{{TFAE}}
:$(1): \quad$ $f$ is continuous
:$(2): \quad$ $f$ is upper semicontinuous
:$(3): \quad$ for each $x \in C$, there exists an open neighborhood $U$ of $x$ such that $\sup \set {\map f x : x \in U} < \infty$
:$(4): \quad$ for some $x_0 \in C$, there exists an open neighborhood $U_0$ of $x_0$ such that $\sup \set {\map f x : x \in U_0} < \infty$
:$(5): \quad$ for some $x_0 \in C$, $f$ is continuous at $x_0$.

Proof:
=== $(1)$ implies $(2)$ ===
This follows from Continuity implies Upper Semicontinuity.
{{qed|lemma}}
Theorem: Continuity implies Upper Semicontinuity

Let $\struct {S, \tau}$ be a topological space.
Let $f : S \to \R$ be a continuous function.
Then $f$ is upper semicontinuous.

Proof:
Let $x_0 \in S$.
Let $\map \mho {x_0}$ be the set of open neighborhoods of $x_0$.
Let $\epsilon > 0$. 
Since $f$ is continuous, it is continuous at $x_0$.
From the definition of continuity at $x_0$, there exists an open neighborhood $U$ of $x_0$ such that:
:$f \sqbrk U \subseteq \openint {\map f {x_0} - \epsilon} {\map f {x_0} + \epsilon}$
Hence we have:
:$\ds \sup_{x \mathop \in U} \map f x < \map f {x_0} + \epsilon$
Hence:
{{begin-eqn}}
{{eqn	| l = \limsup_{x \mathop \to x_0} \map f x
		| r = \inf_{V \in \map \mho {x_0} } \paren {\sup_{x \mathop \in V} \map f x}
}}
{{eqn	| o = \le
		| r = \sup_{x \mathop \in U} \map f x 
}}
{{eqn	| o = <
		| r = \map f {x_0} + \epsilon 
}}
{{end-eqn}}
Since this holds for all $\epsilon > 0$, we have:
:$\ds \limsup_{x \mathop \to x_0} \map f x \le \map f {x_0}$
From Upper Limit of Function is Bounded Below by Value at Limit Point: Corollary, we have that $f$ is upper semicontinuous at $x_0$.
Since $x_0 \in S$ was arbitrary, we have that $f$ is upper semicontinuous.
{{qed}}
Category:Upper Semicontinuity
k36e8603rw7asyefdnqfynvvrp7hfsb
Theorem: Upper Limit of Function is Bounded Below by Value at Limit Point

Let $\struct {X, \tau}$ be a topological space.
Let $f : X \to \overline \R$ be a function.
Let $\limsup$ be the upper limit.
Let $x_0 \in X$.
Then we have:
:$\ds \map f {x_0} \le \limsup_{x \mathop \to x_0} \map f x$

Proof:
Let $\map \mho {x_0}$ be the set of open neighborhoods of $x_0$ in $\struct {X, \tau}$.
Then for each $V \in \map \mho {x_0}$, we have:
:$\ds \sup_{x \mathop \in V} \map f x \ge \map f {x_0}$
since $x_0 \in V$. 
Hence:
:$\ds \inf_{V \in \map \mho {x_0} } \paren {\sup_{x \mathop \in V} \map f x} \ge \map f {x_0}$ 
Hence by the definition of the upper limit, we have:
:$\ds \map f {x_0} \le \limsup_{x \mathop \to x_0} \map f x$
{{qed}}
Category:Limits of Mappings
Category:Upper Limit of Function is Bounded Below by Value at Limit Point
dm6zlac5cxxep3o7lmuzbjcx9dcx169
Theorem: Separation of Non-Empty Set from Set containing Interior Point is Continuous and Proper

Let $\struct {X, \tau}$ be a topological vector space over $\R$.
Let $B \subseteq X$ be a non-empty set.
Let $A \subseteq X$ have non-empty interior $\Int A$ such that there exists a linear functional $f : X \to \R$ and $\alpha \in \R$ with:
:$\map f b \le \alpha \le \map f a$ for each $a \in A$ and $b \in B$. 
That is, the affine hyperplane $\sqbrk {f = \alpha}$ separates $A$ and $B$.
Then $f$ is continuous and the separation is proper.

Proof:
By Non-Zero Linear Functional on Topological Vector Space does not attain Minimum on Interior of Set, we have that $f$ is continuous.
Further, Non-Zero Linear Functional on Topological Vector Space does not attain Minimum on Interior of Set gives that:
:$\map f a > \alpha$ for each $a \in \Int A$.
Since $\Int A \ne \O$, we have that $A \not \subseteq \sqbrk {f = \alpha}$.
Hence the separation is proper.
{{qed}}