This file contains additional general constructions around topological spaces which are useful for properties and theorems.

def PiBase.IsZero {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

We call a set s : Set X in a topological space zero, if there is a continuous function f : X → ℝ such that f ⁻¹' {0} = s

Equations

• PiBase.IsZero s = ∃ (f : C(X, ℝ)), f.toFun ⁻¹' {0} = s

def PiBase.IsCozero {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

We call a set s : Set X in a topological space cozero, if there is a continuous function f : X → ℝ such that f ⁻¹' {0}ᶜ = s

Equations

• PiBase.IsCozero s = ∃ (f : C(X, ℝ)), f.toFun ⁻¹' {0}ᶜ = s

theorem PiBase.IsCozero.isOpen {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsCozero s) : IsOpen s

A cozero set is open.

def PiBase.IsRelativelyCompact {X : Type u} [TopologicalSpace X] (s : Set X) : Prop

Equations

• PiBase.IsRelativelyCompact s = ∀ {ι : Type ?u.1} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → ⋃ (i : ι), U i = Set.univ → ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i

def PiBase.SigmaProduct {ι : Type u_3} {Y : ι → Type u} (x : (i : ι) → Y i) : Set ((i : ι) → Y i)

Σ-product (of topological spaces). Not to be confused with the disjoint union (topological sum).

Equations

• PiBase.SigmaProduct x = {s : (i : ι) → Y i | {i : ι | s i ≠ x i}.Countable}

def PiBase.IsRetract {X : Type u} [TopologicalSpace X] (A : Set X) : Prop

A set s : Set X is called a retract, if there is a continuous map f : X → s such that ∀ x ∈ s, f x = x

Equations

• PiBase.IsRetract A = ∃ (f : C(X, X)), f.comp f = f ∧ A = Set.range ⇑f

def PiBase.IsRegularOpen {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

A set is called regular open if it is equal to the interior of its closure.

Equations

• PiBase.IsRegularOpen s = (interior (closure s) = s)

theorem PiBase.IsRegularOpen.isOpen {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsRegularOpen s) : IsOpen s

A regular open set is open

def PiBase.IsCutPoint {X : Type u_1} [TopologicalSpace X] (p : X) : Prop

A point cut point p in a space, is a space such that X \ {p} is disconnected.

Equations

• PiBase.IsCutPoint p = ¬IsPreconnected {p}ᶜ

theorem PiBase.Homeomorph.isCutPoint {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {p : X} (e : X ≃ₜ Y) (hp : IsCutPoint p) : IsCutPoint (e p)

The image of a cut point under a homeomorphism is a cut point.

def PiBase.InseparableComponent {X : Type u_1} [TopologicalSpace X] (x : X) : Set X

The inseperable component of x : X are the points inseparable to that point.

Equations

• PiBase.InseparableComponent x = {y : X | Inseparable x y}

@[simp]

theorem PiBase.mem_self_inseparableComponent {X : Type u_1} [TopologicalSpace X] (x : X) : x ∈ InseparableComponent x

@[simp]

theorem PiBase.inseparableComponent_nonempty {X : Type u_1} [TopologicalSpace X] {x : X} : (InseparableComponent x).Nonempty

theorem PiBase.inseparableComponent_eq {X : Type u_1} [TopologicalSpace X] {x y : X} (h : Inseparable x y) : InseparableComponent x = InseparableComponent y

theorem PiBase.t0Space_iff_inseparableComponent_eq_singleton {X : Type u_1} [TopologicalSpace X] : T0Space X ↔ ∀ (x : X), InseparableComponent x = {x}

A space is T₀ iff all its inseparable components are trivial.

theorem PiBase.T0Space.inseparableComponent_singleton {X : Type u_1} [TopologicalSpace X] [h : T0Space X] (x : X) : InseparableComponent x = {x}

theorem PiBase.SeparationQuotient.inseparableComponent_preimage {X : Type u_1} [TopologicalSpace X] (x : X) : InseparableComponent x = SeparationQuotient.mk ⁻¹' {SeparationQuotient.mk x}

theorem PiBase.inseparableComponent_of_open {X : Type u_1} [TopologicalSpace X] {x : X} (h : IsOpen {x}) : InseparableComponent x = {x}

theorem PiBase.inseparableComponent_of_closed {X : Type u_1} [TopologicalSpace X] {x : X} (h : IsClosed {x}) : InseparableComponent x = {x}

theorem PiBase.inseparableComponent_subset_open {X : Type u_1} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) (xs : x ∈ s) : InseparableComponent x ⊆ s

theorem PiBase.inseparableComponent_subset_closed {X : Type u_1} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsClosed s) (xs : x ∈ s) : InseparableComponent x ⊆ s

theorem PiBase.IsIrreducible.inseparableComponent {X : Type u_1} [TopologicalSpace X] (x : X) : IsIrreducible (InseparableComponent x)

The inseparable component is irreducible.

theorem PiBase.subsingleton_iff_singleton_univ {α : Type u} (a : α) : Subsingleton α ↔ Set.univ = {a}

class PiBase.Symmetric (α : Type u) extends Dist α : Type u

A symmetric for of a set.

• dist : α → α → ℝ
• dist_nonneg (x y : α) : 0 ≤ dist x y
• dist_self (x : α) : dist x x = 0
• dist_comm (x y : α) : dist x y = dist y x
• eq_of_dist_eq_zero {x y : α} : dist x y = 0 → x = y

def PiBase.Symmetric.ball {ι : Type u_3} [Symmetric ι] (i : ι) (ε : ℝ) : Set ι

A ball for a symmetric.

Equations

• PiBase.Symmetric.ball i ε = {x : ι | dist x i ≤ ε}

class PiBase.SemimetricSpace (X : Type u) [TopologicalSpace X] extends PiBase.Symmetric X : Type u

A semimetric space

• dist : X → X → ℝ
• dist_nonneg (x y : X) : 0 ≤ dist x y
• dist_self (x : X) : dist x x = 0
• dist_comm (x y : X) : dist x y = dist y x
• eq_of_dist_eq_zero {x y : X} : dist x y = 0 → x = y
• symmetric_nbhd (x : X) : (nhds x).HasBasis (fun (ε : ℝ) => 0 < ε) (Symmetric.ball x)

class PiBase.SymmetricSpace (X : Type u) [TopologicalSpace X] extends PiBase.Symmetric X : Type u

A symmetric space

• dist : X → X → ℝ
• dist_nonneg (x y : X) : 0 ≤ dist x y
• dist_self (x : X) : dist x x = 0
• dist_comm (x y : X) : dist x y = dist y x
• eq_of_dist_eq_zero {x y : X} : dist x y = 0 → x = y
• isOpen_iff (s : Set X) : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Symmetric.ball x ε ⊆ s

@[reducible, inline]

abbrev PiBase.SemimetricSpace.symmetricSpace (X : Type u) [TopologicalSpace X] [h : SemimetricSpace X] : SymmetricSpace X

Every semimetric space is a symmetric space.

Equations

• PiBase.SemimetricSpace.symmetricSpace X = { toSymmetric := h.toSymmetric, isOpen_iff := ⋯ }

def PiBase.IsInjPathConnected {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

A set s : Set X is called injectively path connected, if for any two point in s there is an injective path in x joining them.

Equations

• PiBase.IsInjPathConnected s = Pairwise fun (x y : X) => x ∈ s → y ∈ s → ∃ (f : Path x y), Function.Injective ⇑f ∧ Set.range ⇑f ⊆ s

theorem PiBase.IsInjPathConnected.isPathConnected {X : Type u_1} [TopologicalSpace X] {s : Set X} (h : IsInjPathConnected s) (hs : s.Nonempty) : IsPathConnected s

An injectively path connected set is path connected.

def PiBase.HasTrivialFundGroupImageAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : X) : Prop

A proposition for when the image of the fundamental group at x : X under f: X → Y is trivial.

Equations

• PiBase.HasTrivialFundGroupImageAt f x = ((FundamentalGroup.map f x).range = ⊥)