ExtremallyDisconnected.open_closure
theorem ExtremallyDisconnected.open_closure :
∀ {X : Type u} [inst : TopologicalSpace X] [self : ExtremallyDisconnected X] (U : Set X),
IsOpen U → IsOpen (closure U)
The theorem `ExtremallyDisconnected.open_closure` states that for any type `X` equipped with a topological space structure and the property of being extremally disconnected, any set `U` of `X` that is open has the property that its closure is also open. Here, the closure of a set is defined as the smallest closed set containing the set, and the openness of a set is subject to the definition of open sets in the ambient topological space. In other words, in an extremally disconnected topological space, the closure of any open set remains open.
More concisely: In an extremally disconnected topological space, the closure of any open set is open.
|
ExtremallyDisconnected.disjoint_closure_of_disjoint_isOpen
theorem ExtremallyDisconnected.disjoint_closure_of_disjoint_isOpen :
∀ {A : Type u} [inst : TopologicalSpace A] [inst_1 : ExtremallyDisconnected A] {U₁ U₂ : Set A},
Disjoint U₁ U₂ → IsOpen U₁ → IsOpen U₂ → Disjoint (closure U₁) (closure U₂)
This theorem, Lemma 2.2 in Gleason's *Projective topological spaces*, states that in an extremally disconnected space, if $U_1$ and $U_2$ are two disjoint open sets, then their closures, $\overline{U_1}$ and $\overline{U_2}$ respectively, are also disjoint. Here, a set is said to be open in the surrounding topological space, and two sets are called disjoint if their intersection is the bottom element. The closure of a set is the smallest closed set that contains it. "Extremally disconnected" refers to a specific property of the topological space.
More concisely: In an extremally disconnected topological space, the closures of two disjoint open sets are also disjoint.
|
exists_compact_surjective_zorn_subset
theorem exists_compact_surjective_zorn_subset :
∀ {A D : Type u} [inst : TopologicalSpace A] [inst_1 : TopologicalSpace D] [inst_2 : T1Space A]
[inst_3 : CompactSpace D] {π : D → A},
Continuous π →
Function.Surjective π →
∃ E,
CompactSpace ↑E ∧
π '' E = Set.univ ∧ ∀ (E₀ : Set ↑E), E₀ ≠ Set.univ → IsClosed E₀ → E.restrict π '' E₀ ≠ Set.univ
This theorem, referenced as Lemma 2.4 in Gleason's "Projective Topological Spaces", states that given a continuous surjective function `π` from a compact space `D` to a Fréchet space `A`, there exists a compact subset `E` of `D`, such that `π` maps `E` onto `A` and satisfies the "Zorn subset condition". The "Zorn subset condition" is defined as follows: for any proper closed subset `E₀` of `E`, the image of `E₀` under `π` is not equal to `A`. In other words, `π(E₀)` does not cover the entire space `A`.
More concisely: Given a continuous surjective function from a compact space onto a Fréchet space, there exists a compact subset such that its image under the function does not cover the entire space and properly intersects every other image of proper closed subsets.
|
CompactT2.Projective.extremallyDisconnected
theorem CompactT2.Projective.extremallyDisconnected :
∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] [inst_2 : T2Space X],
CompactT2.Projective X → ExtremallyDisconnected X
This theorem states that for any type `X` equipped with a topological space structure, if `X` is a compact Hausdorff space (also known as a T2 space), and if `X` is projective in the sense of the CompactT2 theory, then `X` is extremally disconnected. In topological terms, an extremally disconnected space is one where the closure of every open set is open.
More concisely: If `X` is a compact Hausdorff and projective space in the sense of the CompactT2 theory, then `X` is an extremally disconnected topological space.
|
CompactT2.ExtremallyDisconnected.projective
theorem CompactT2.ExtremallyDisconnected.projective :
∀ {A : Type u} [inst : TopologicalSpace A] [inst_1 : ExtremallyDisconnected A] [inst_2 : CompactSpace A]
[inst_3 : T2Space A], CompactT2.Projective A
This theorem, which is Theorem 2.5 in Gleason's "Projective topological spaces", states that in the category of compact spaces with continuous maps, a space is a projective space if and only if it is extremally disconnected. This applies to any type `A` which has a topological space structure, is extremally disconnected, is compact, and satisfies the T2 separation axiom (also known as being a Hausdorff space).
More concisely: A compact, Hausdorff space is a projective space if and only if it is extremally disconnected.
|
image_subset_closure_compl_image_compl_of_isOpen
theorem image_subset_closure_compl_image_compl_of_isOpen :
∀ {A E : Type u} [inst : TopologicalSpace A] [inst_1 : TopologicalSpace E] {ρ : E → A},
Continuous ρ →
Function.Surjective ρ →
(∀ (E₀ : Set E), E₀ ≠ Set.univ → IsClosed E₀ → ρ '' E₀ ≠ Set.univ) →
∀ {G : Set E}, IsOpen G → ρ '' G ⊆ closure (ρ '' Gᶜ)ᶜ
This theorem, Lemma 2.1 in Gleason's "Projective Topological Spaces", states that for any two topological spaces `A` and `E`, if there is a continuous surjective function `ρ` from `E` to `A` that satisfies the Zorn subset condition (i.e., for any subset `E₀` of `E` that is not the universal set and is closed in `E`, the image of `E₀` under `ρ` is not the universal set of `A`), then for any open set `G` in `E`, the image of `G` under `ρ` is a subset of the closure of the complement of the image of the complement of `G` under `ρ`. In mathematical terms, if `ρ: E -> A` is a continuous surjection that satisfies the Zorn subset condition, then for any open set `G ⊆ E`, we have `ρ(G) ⊆ closure(A \ ρ(E \ G))`.
More concisely: Given a continuous surjective function `ρ: E -> A` between topological spaces `E` and `A` satisfying the Zorn subset condition, the image of any open set `G ⊆ E` is a subset of the closure of the complement of the image of the complement of `G` under `ρ`, that is, `ρ(G) ⊆ closure(A \ ρ(E \ G))`.
|