2.1 Leroy Chapter V

Lemma 48 (1.10) Intersection of Open and Closed Sublocals

For any \(U \in O(E)\), and sublocal \(X\) of \(E\) we have:

\[ e_{U \cap X} = e_Ue_X \]

And for a closed \(F\)

\[ e_{X \cap F} = e_Xe_F \]

Lemma 49 Regular Top to regular local

Any regular topological space induces a regular local.

Lemma 50 Opens

(Leroy V.1 Remarque 2) The Open subsets of any good enough topological space correspond precisely to the open sublocals of the corresponding local.

Lemma 51 Subset Sublocal

(leroy V.1 Remarque 3) Any subset \(X\) of a good enough topological space \(E\) induces a sublocal \([X]\) of the corresponding local. This is an order preserving embedding.

Definition 52 Good enough topological space

blackbox to mathlib????

Lemma 53 Subset to sublocal Part 1

(Leroy Proposition 5.1.1)

For two subspaces \(X\) and \(Y\) of \(E\) and an open subspaces \(U\) of \(E\), we have:

\(X \subset Y \implies [X] \subset [Y]\)
\(X \subset U \iff [X] \subset [U]\)
If \(E\) is a good enough topological space, then

\[ X \subset Y \iff [X] \subset [Y] \]

Lemma 54 Subset to sublocal Part 2

(Leroy Proposition 5.1.2, 5.1.3) For an open subspace \(U\) of \(E\) and a subspace \(X\) of \(E\), we have:

\begin{gather*} [U \cap X] = [U] \cap [X]\\ F = E \setminus U\\[F] = [E] \\[U] = [X] \cap [F]\\ \end{gather*}

Lemma 55 Part 3

For any subspaces \(X\) of E, we have:

\[ Ext[X] = [Ext X] \]
\[ \bar{[X]} = [\bar{X}] \]
\[ [Int X] \subset Int[X] \]
\[ \partial [X] \subset [Fr(X)] \]

For a good enough topological space \(E\), we have equality in 3 and 4.

Proposition 56 Subset to sublocal preserves structure

For two subspaces \(X\) and \(Y\) of \(E\) and an open subspaces \(U\) of \(E\), we have:

\(X \subset Y \implies [X] \subset [Y]\)
\(X \subset U \iff [X] \subset [U]\)
If \(E\) is a good enough topological space, then

\[ X \subset Y \iff [X] \subset [Y] \]
\[ [U \cap X] = [U] \cap [X] \]
\(\dots \)

Theorem 57 Measure top to loc

Any measure on a good enough topological space \(X\) induces a measure on the corresponding local. Furthermore, the classical caratheodory extension onto \(\mathcal{P}(X)\) agrees with the restriction of the caratheodory extension of the induced measure on the local.

Hello