From 65e5a741655d8339ad5763e365ea2addd2e96e51 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Fri, 9 Aug 2024 15:15:49 +0200 Subject: put cardinalit to the right place --- library/cardinal.tex | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'library/cardinal.tex') diff --git a/library/cardinal.tex b/library/cardinal.tex index d0dec59..8691b30 100644 --- a/library/cardinal.tex +++ b/library/cardinal.tex @@ -3,6 +3,7 @@ \import{set.tex} \import{ordinal.tex} \import{function.tex} +\import{numbers.tex} \begin{definition}\label{finite} $X$ is finite iff there exists a natural number $k$ such that @@ -12,3 +13,8 @@ \begin{abbreviation}\label{infinite} $X$ is infinite iff $X$ is not finite. \end{abbreviation} + +\begin{definition}\label{cardinality} + $X$ has cardinality $k$ iff $k$ is a natural number and + there exists a bijection from $k$ to $X$. +\end{definition} -- cgit v1.2.3 From 34aad4be8fb8433f0205517732da0d449d077572 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sat, 10 Aug 2024 19:18:39 +0200 Subject: more more urysohn --- library/cardinal.tex | 2 + library/topology/urysohn.tex | 341 ++++++++++++++++++++++++------------------- 2 files changed, 190 insertions(+), 153 deletions(-) (limited to 'library/cardinal.tex') diff --git a/library/cardinal.tex b/library/cardinal.tex index 8691b30..044e5d1 100644 --- a/library/cardinal.tex +++ b/library/cardinal.tex @@ -18,3 +18,5 @@ $X$ has cardinality $k$ iff $k$ is a natural number and there exists a bijection from $k$ to $X$. \end{definition} + + diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index 3152de7..028e10f 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -198,60 +198,82 @@ The first tept will be a formalisation of chain constructions. Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. Suppose $A \inter B$ is empty. - Suppose $U = \{A,(X \setminus B)\}$. - Suppose $\indexset[U]= \{\zero, 1\}$. - Suppose $\index[U](\zero) = A$. - Suppose $\index[U](1) = (X \setminus B)$. - Then $U$ is a urysohnchain in $X$. + Then there exist $U$ + such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$ + and $\indexset[U]= \{\zero, 1\}$ + and $\index[U](\zero) = A$ + and $\index[U](1) = (\carrier[X] \setminus B)$. + %$U$ is a urysohnchain in $X$. \end{proposition} \begin{proof} - We show that $U$ is a sequence. - \begin{subproof} - Omitted. - \end{subproof} - We show that $A \subseteq (X \setminus B)$. - \begin{subproof} - Omitted. - \end{subproof} + Omitted. - We show that $U$ is a chain of subsets. - \begin{subproof} - For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$. - It suffices to show that for all $n \in \indexset[U]$ we have - for all $m \in \indexset[U]$ such that - $n < m$ we have $\index[U](n) \subseteq \index[U](m)$. - Fix $n \in \indexset[U]$. - Fix $m \in \indexset[U]$. - \begin{byCase} - \caseOf{$n = 1$.} Trivial. - \caseOf{$n = \zero$.} - \begin{byCase} - \caseOf{$m = \zero$.} Trivial. - \caseOf{$m = 1$.} Omitted. - \end{byCase} - \end{byCase} - \end{subproof} + % We show that $U$ is a sequence. + % \begin{subproof} + % Omitted. + % \end{subproof} +% + % We show that $A \subseteq (\carrier[X] \setminus B)$. + % \begin{subproof} + % Omitted. + % \end{subproof} +% + % We show that $U$ is a chain of subsets. + % \begin{subproof} + % For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$. + % It suffices to show that for all $n \in \indexset[U]$ we have + % for all $m \in \indexset[U]$ such that + % $n < m$ we have $\index[U](n) \subseteq \index[U](m)$. + % Fix $n \in \indexset[U]$. + % Fix $m \in \indexset[U]$. + % \begin{byCase} + % \caseOf{$n = 1$.} Trivial. + % \caseOf{$n = \zero$.} + % \begin{byCase} + % \caseOf{$m = \zero$.} Trivial. + % \caseOf{$m = 1$.} Omitted. + % \end{byCase} + % \end{byCase} + % \end{subproof} +% + % $A \subseteq X$. + % $(X \setminus B) \subseteq X$. + % We show that for all $x \in U$ we have $x \subseteq X$. + % \begin{subproof} + % Omitted. + % \end{subproof} +% + % We show that $\closure{A}{X} \subseteq \interior{(X \setminus B)}{X}$. + % \begin{subproof} + % Omitted. + % \end{subproof} + % We show that for all $n,m \in \indexset[U]$ such that $n < m$ we have + % $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$. + % \begin{subproof} + % Omitted. + % \end{subproof} - $A \subseteq X$. - $(X \setminus B) \subseteq X$. - We show that for all $x \in U$ we have $x \subseteq X$. - \begin{subproof} - Omitted. - \end{subproof} + +\end{proof} - We show that $\closure{A}{X} \subseteq \interior{(X \setminus B)}{X}$. - \begin{subproof} - Omitted. - \end{subproof} - We show that for all $n,m \in \indexset[U]$ such that $n < m$ we have - $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$. - \begin{subproof} - Omitted. - \end{subproof} +\begin{proposition}\label{urysohnchain_induction_begin_step_two} + Let $X$ be a urysohn space. + Suppose $A,B \in \closeds{X}$. + Suppose $A \inter B$ is empty. + Suppose there exist $U$ + such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$ + and $\indexset[U]= \{\zero, 1\}$ + and $\index[U](\zero) = A$ + and $\index[U](1) = (\carrier[X] \setminus B)$. + Then $U$ is a urysohnchain in $X$. +\end{proposition} +\begin{proof} + Omitted. \end{proof} + \begin{proposition}\label{t_four_propositon} Let $X$ be a urysohn space. Then for all $A,B \subseteq X$ such that $\closure{A}{X} \subseteq \interior{B}{X}$ @@ -295,134 +317,147 @@ The first tept will be a formalisation of chain constructions. \end{proof} +\begin{proposition}\label{existence_of_staircase_function} + Let $X$ be a urysohn space. + Suppose $U$ is a urysohnchain in $X$ and $U$ has cardinality $k$. + Suppose $k \neq \zero$. + Then there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ + and for all $n \in \indexset[U]$ we have for all $x \in \index[U](n)$ + we have $f(x) = \rfrac{n}{k}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} +\begin{abbreviation}\label{refinment_abbreviation} + $x \refine y$ iff $x$ is a refinmant of $y$. +\end{abbreviation} - - -% The next thing we need to define is the uniform staircase function. -% This function has it's domain in $X$ and maps to the closed interval $[0,1]$. -% These functions should behave als follows, -% \begin{align} -% &f(A_{0}) = 1 &\text{consant} \\ -% &f(A_{k} \setminus A_{k+1}) = 1-\frac{k}{r} &\text{constant.} -% \end{align} - -% We then prove that for any given $r$ we find a repolished chain, -% which contains the $A_{i}$ and this replished chain is also legal. -% -% The proof will be finished by taking the limit on $f_{n}$ with $f_{n}$ -% be a staircase function with $n$ many refinemants. -% This limit will be continuous and we would be done. - - -% TODO: Since we want to prove that $f$ is continus, we have to formalize that -% \reals with the usual topology is a topological space. -% ------------------------------------------------------------- - \begin{theorem}\label{urysohn} Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. Suppose $A \inter B$ is empty. - There exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ + There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. \end{theorem} \begin{proof} - We show that for all $n \in \naturals$ we have - if there exist $C$ such that $C$ is a urysohnchain in $X$ of cardinality $n$ - then there exist $C'$ such that $C'$ is a urysohnchain in $X$ of cardinality $n+1$ - and $C'$ is a refinmant of $C$. - \begin{subproof} - Omitted. - \end{subproof} - - There exist $\eta$ such that $\eta$ is a urysohnchain in $X$ and $\eta =\{A, (x \setminus B)\}$. - - - Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$. + There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ + and $\indexset[\eta] = \{\zero, 1\}$ + and $\index[\eta](\zero) = A$ + and $\index[\eta](1) = (\carrier[X] \setminus B)$ by \cref{urysohnchain_induction_begin}. - We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence - and for all $i \in \indexset[\zeta]$ we have - $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$ - and $A \subseteq \index[\zeta](i)$ - and $\index[\zeta](i) \subseteq (X \setminus B)$ - and for all $j \in \indexset[\zeta]$ such that - $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$. + We show that there exist $\zeta$ such that $\zeta$ is a sequence + and $\indexset[\zeta] = \naturals$ + and $\eta \in \carrier[\zeta]$ and $\index[\zeta](\eta) = \zero$ + and for all $n \in \indexset[\zeta]$ we have $n+1 \in \indexset[\zeta]$ + and $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)$. \begin{subproof} - Omitted. - \end{subproof} - - - - - - + %Let $P = \{ n \in \naturals \mid \exists \zeta. ((n = \zero \land \index[\zeta](n) = \eta \land \index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)) \lor (n \neq \zero \land \index[\zeta](n)$ is a urysohnchain in $X$ \land $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)))\}$. + %Let $C = \{ x \mid \text{$x$ is a uysohncahin in $X$}\}$. + Let $\alpha = \{x \in C \mid \exists y \in \alpha. x \refine y \lor x = \eta\}$. + Let $\beta = \{ (n,x) \mid n \in \naturals \mid \exists m \in \naturals. \exists y \in \alpha. (x \in \alpha) \land ((x \refine y \land m = n+1 )\lor ((n,x) = (\zero,\eta)))\}$. - - We show that there exist $g \in \funs{X}{\intervalclosed{\zero}{1}}$ such that $g(A)=1$ and $g(X\setminus A) = \zero$. - \begin{subproof} - Omitted. + % TODO: Proof that \beta is a function which would be used for the indexing. + \end{subproof} - $g$ is a staircase function and $\chain[g] = C$. - $g$ is a legal staircase function. - We show that there exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ - and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. - \begin{subproof} - Omitted. - \end{subproof} - %We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$. - %\begin{subproof} - % Omitted. - %\end{subproof} - - %Proof Sheme Idea: - % -We proof for n=1 that C_{n} is a chain and legal - % -Then by induction with P(n+1) is refinmant of P(n) - % -Therefore we have a increing refinmant of these Chains such that our limit could even apply - % --------------------------------------------------------- - - %We show that there exist $f \in \funs{\naturals}{\funs{X}{\intervalclosed{0}{1}}}$ such that $f(n)$ is a staircase function. %TODO: Define Staircase function - %\begin{subproof} - % Omitted. - %\end{subproof} - - - % Formalization idea of enumarted sequences: - % - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} - % - This should give all finite and infinte enumarable sequences - % - Introduce a notion for the indexing of these enumarable sequences. - % - Then we can define the limit of a enumarted sequence of functions. - % --------------------------------------------------------- - % - % Here we need a limit definition for sequences of functions - %We show that there exist $F \in \funs{X}{\intervalclosed{0}{1}}$ such that $F = \limit{set of the staircase functions}$ - %\begin{subproof} - % Omitted. - %\end{subproof} - % - %We show that $F(A) = 1$. - %\begin{subproof} - % Omitted. - %\end{subproof} - % - %We show that $F(B) = 0$. - %\begin{subproof} - % Omitted. - %\end{subproof} - % - %We show that $F$ is continuous. - %\begin{subproof} - % Omitted. - %\end{subproof} + %Suppose $\eta$ is a urysohnchain in $X$. + %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$ + %and $\indexset[\eta] = \{\zero, 1\}$ + %and $\index[\eta](\zero) = A$ + %and $\index[\eta](1) = (X \setminus B)$. + + + %Then $\eta$ is a urysohnchain in $X$. + + % Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$. + % + % We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence + % and for all $i \in \indexset[\zeta]$ we have + % $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$ + % and $A \subseteq \index[\zeta](i)$ + % and $\index[\zeta](i) \subseteq (X \setminus B)$ + % and for all $j \in \indexset[\zeta]$ such that + % $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$. + % \begin{subproof} + % Omitted. + % \end{subproof} + % + % + % + % + % + % + % + % + % We show that there exist $g \in \funs{X}{\intervalclosed{\zero}{1}}$ such that $g(A)=1$ and $g(X\setminus A) = \zero$. + % \begin{subproof} + % Omitted. + % \end{subproof} + % $g$ is a staircase function and $\chain[g] = C$. + % $g$ is a legal staircase function. + % + % + % We show that there exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ + % and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. + % \begin{subproof} + % Omitted. + % \end{subproof} + + + % We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$. + % \begin{subproof} + % Omitted. + % \end{subproof} + + % Proof Sheme Idea: + % -We proof for n=1 that C_{n} is a chain and legal + % -Then by induction with P(n+1) is refinmant of P(n) + % -Therefore we have a increing refinmant of these Chains such that our limit could even apply + % --------------------------------------------------------- + + % We show that there exist $f \in \funs{\naturals}{\funs{X}{\intervalclosed{0}{1}}}$ such that $f(n)$ is a staircase function. %TODO: Define Staircase function + % \begin{subproof} + % Omitted. + % \end{subproof} + + + % Formalization idea of enumarted sequences: + % - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} + % - This should give all finite and infinte enumarable sequences + % - Introduce a notion for the indexing of these enumarable sequences. + % - Then we can define the limit of a enumarted sequence of functions. + % --------------------------------------------------------- + % + % Here we need a limit definition for sequences of functions + % We show that there exist $F \in \funs{X}{\intervalclosed{0}{1}}$ such that $F = \limit{set of the staircase functions}$ + % \begin{subproof} + % Omitted. + % \end{subproof} + % + % We show that $F(A) = 1$. + % \begin{subproof} + % Omitted. + % \end{subproof} + % + % We show that $F(B) = 0$. + % \begin{subproof} + % Omitted. + % \end{subproof} + % + % We show that $F$ is continuous. + % \begin{subproof} + % Omitted. + % \end{subproof} \end{proof} -\begin{theorem}\label{safe} - Contradiction. -\end{theorem} +%\begin{theorem}\label{safe} +% Contradiction. +%\end{theorem} -- cgit v1.2.3 From f6b22fd533bd61e9dbcb6374295df321de99b1f2 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 23 Sep 2024 03:05:41 +0200 Subject: Abgabe --- library/algebra/group.tex | 2 +- library/algebra/monoid.tex | 2 +- library/cardinal.tex | 2 +- library/numbers.tex | 2 +- library/topology/basis.tex | 2 +- library/topology/continuous.tex | 2 ++ library/topology/metric-space.tex | 4 ++-- library/topology/real-topological-space.tex | 2 +- library/topology/separation.tex | 2 ++ library/topology/topological-space.tex | 2 +- library/topology/urysohn.tex | 4 ++-- library/topology/urysohn2.tex | 18 ++++++++++++++---- 12 files changed, 29 insertions(+), 15 deletions(-) (limited to 'library/cardinal.tex') diff --git a/library/algebra/group.tex b/library/algebra/group.tex index 7de1051..449bacb 100644 --- a/library/algebra/group.tex +++ b/library/algebra/group.tex @@ -1,5 +1,5 @@ \import{algebra/monoid.tex} -\section{Group} +\section{Group}\label{form_sec_group} \begin{struct}\label{group} A group $G$ is a monoid such that diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex index 06fcb50..3249a93 100644 --- a/library/algebra/monoid.tex +++ b/library/algebra/monoid.tex @@ -1,5 +1,5 @@ \import{algebra/semigroup.tex} -\section{Monoid} +\section{Monoid}\label{form_sec_monoid} \begin{struct}\label{monoid} A monoid $A$ is a semigroup equipped with diff --git a/library/cardinal.tex b/library/cardinal.tex index 044e5d1..5682619 100644 --- a/library/cardinal.tex +++ b/library/cardinal.tex @@ -1,4 +1,4 @@ -\section{Cardinality} +\section{Cardinality}\label{form_sec_cardinality} \import{set.tex} \import{ordinal.tex} diff --git a/library/numbers.tex b/library/numbers.tex index ac0a683..d3af3f1 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -4,7 +4,7 @@ \import{ordinal.tex} -\section{The real numbers} +\section{The numbers}\label{form_sec_numbers} \begin{signature} $\reals$ is a set. diff --git a/library/topology/basis.tex b/library/topology/basis.tex index 052c551..f0f77e4 100644 --- a/library/topology/basis.tex +++ b/library/topology/basis.tex @@ -2,7 +2,7 @@ \import{set.tex} \import{set/powerset.tex} -\subsection{Topological basis} +\subsection{Topological basis}\label{form_sec_topobasis} \begin{abbreviation}\label{covers} $C$ covers $X$ iff diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex index a9bc58e..95c4d0a 100644 --- a/library/topology/continuous.tex +++ b/library/topology/continuous.tex @@ -3,6 +3,8 @@ \import{function.tex} \import{set.tex} +\subsection{Continuous}\label{form_sec_continuous} + \begin{definition}\label{continuous} $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$. \end{definition} diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex index 0ed7bab..031aa0f 100644 --- a/library/topology/metric-space.tex +++ b/library/topology/metric-space.tex @@ -4,10 +4,10 @@ \import{set/powerset.tex} \import{topology/basis.tex} -\section{Metric Spaces} +\section{Metric Spaces}\label{form_sec_metric} \begin{definition}\label{metric} - $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reaaals$ and + $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and for all $x,y,z \in M$ we have $f(x,x) = \zero$ and $f(x,y) = f(y,x)$ and diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex index c76fd46..db7ee94 100644 --- a/library/topology/real-topological-space.tex +++ b/library/topology/real-topological-space.tex @@ -11,7 +11,7 @@ \import{function.tex} -\section{Topology Reals} +\section{Topology Reals}\label{form_sec_toporeals} \begin{definition}\label{topological_basis_reals_eps_ball} $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$. diff --git a/library/topology/separation.tex b/library/topology/separation.tex index 0c68290..aaa3907 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -1,6 +1,8 @@ \import{topology/topological-space.tex} \import{set.tex} +\subsection{Separation}\label{form_sec_separation} + % T0 separation \begin{definition}\label{is_kolmogorov} $X$ is Kolmogorov iff diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex index f8bcb93..409e107 100644 --- a/library/topology/topological-space.tex +++ b/library/topology/topological-space.tex @@ -2,7 +2,7 @@ \import{set/powerset.tex} \import{set/cons.tex} -\section{Topological spaces} +\section{Topological spaces}\label{form_sec_topospaces} \begin{struct}\label{topological_space} A topological space $X$ is a onesorted structure equipped with diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index ae03273..cd85fbc 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -13,7 +13,7 @@ \import{set/fixpoint.tex} \import{set/product.tex} -\section{Urysohns Lemma} +\section{Urysohns Lemma Part 1 with struct}\label{form_sec_urysohn1} % In this section we want to proof Urysohns lemma. % We try to follow the proof of Klaus Jänich in his book. TODO: Book reference % The Idea is to construct staircase functions as a chain. @@ -22,7 +22,7 @@ %Chains of sets. -The first tept will be a formalisation of chain constructions. +This is the first attempt to prove Urysohns Lemma with the usage of struct. \subsection{Chains of sets} % Assume $A,B$ are subsets of a topological space $X$. diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 08841da..a1a3ba0 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -15,7 +15,7 @@ \import{topology/real-topological-space.tex} \import{set/equinumerosity.tex} -\section{Urysohns Lemma} +\section{Urysohns Lemma}\label{form_sec_urysohn} @@ -891,15 +891,25 @@ \begin{byCase} \caseOf{$x \in (\carrier[X] \setminus \closure{\at{U'}{\max{\dom{U'}}}}{X})$.} Therefore $x \notin \closure{\at{U'}{\max{\dom{U'}}}}{X}$. - Therefore $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$. + We show that $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$. + \begin{subproof} + Omitted. + \end{subproof} Therefore $x \notin (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$. - Then $g(x) = 1$ . + We show that $g(x) = 1$. + \begin{subproof} + Omitted. + \end{subproof} \caseOf{$x \in \closure{\at{U'}{\max{\dom{U'}}}}{X}$.} \begin{byCase} \caseOf{$x \in \closure{\at{U'}{\min{\dom{U'}}}}{X}$.} - $g(x) = \zero$. + We show that $g(x) = \zero$. + \begin{subproof} + Omitted. + \end{subproof} \caseOf{$x \in (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.} Then $g(x)$ is the staircase step value at $x$ of $U'$ in $X$. + Omitted. \end{byCase} \end{byCase} -- cgit v1.2.3