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

noncomputable def PiBase.Spread (X : Type u) [TopologicalSpace X] : Cardinal.{u}

Spread of a topological space

Equations

• PiBase.Spread X = sSup {t : Cardinal.{?u.1} | ∃ (D : Set X), Cardinal.mk ↑D = t ∧ IsDiscrete D} + Cardinal.aleph0

theorem PiBase.upperBounds_spread (X : Type u) [TopologicalSpace X] : Cardinal.mk X ∈ upperBounds {t : Cardinal.{u} | ∃ (D : Set X), Cardinal.mk ↑D = t ∧ IsDiscrete D}

theorem PiBase.bddAbove_spread (X : Type u) [TopologicalSpace X] : BddAbove {t : Cardinal.{u} | ∃ (D : Set X), Cardinal.mk ↑D = t ∧ IsDiscrete D}

theorem PiBase.spread_le_card (X : Type u) [TopologicalSpace X] : Spread X ≤ Cardinal.mk X + Cardinal.aleph0

The spread is less then the cardinality of the space + ℵ₀.

noncomputable def PiBase.Extent (X : Type u) [TopologicalSpace X] : Cardinal.{u}

Spread of a topological space

Equations

• PiBase.Extent X = sSup {t : Cardinal.{?u.1} | ∃ (D : Set X), Cardinal.mk ↑D = t ∧ IsClosed D ∧ IsDiscrete D} + Cardinal.aleph0

theorem PiBase.upperBounds_extent (X : Type u) [TopologicalSpace X] : Cardinal.mk X ∈ upperBounds {t : Cardinal.{u} | ∃ (D : Set X), Cardinal.mk ↑D = t ∧ IsClosed D ∧ IsDiscrete D}

theorem PiBase.bddAbove_extent (X : Type u) [TopologicalSpace X] : BddAbove {t : Cardinal.{u} | ∃ (D : Set X), Cardinal.mk ↑D = t ∧ IsClosed D ∧ IsDiscrete D}

theorem PiBase.extent_le_spread (X : Type u) [TopologicalSpace X] : Extent X ≤ Spread X

The extent of a space is less or equal to the spread.

theorem PiBase.aleph_zero_le_extent (X : Type u) [TopologicalSpace X] : Cardinal.aleph0 ≤ Extent X

The extent of a space is at least ℵ₀.

theorem PiBase.aleph_zero_le_spread (X : Type u) [TopologicalSpace X] : Cardinal.aleph0 ≤ Spread X

The spread of a space is at least ℵ₀.

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

A radially closed set is a set such that all limits of transfinite of sequences in the set lie in the set themselves

Equations

• PiBase.IsRadiallyClosed s = ∀ (x : X), (∃ (o : Ordinal.{?u.1}) (f : ↑(Set.Iio o) → X), 0 < o ∧ Set.range f ⊆ s ∧ Filter.Tendsto f Filter.atTop (nhds x)) → x ∈ s

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

The radial closure of a set.

Equations

• PiBase.radialClosure s = {x : X | ∃ (o : Ordinal.{?u.1}) (f : ↑(Set.Iio o) → X), 0 < o ∧ Set.range f ⊆ s ∧ Filter.Tendsto f Filter.atTop (nhds x)}

theorem PiBase.seqClosure_subset_radialClosure {X : Type u} [TopologicalSpace X] {s : Set X} : seqClosure s ⊆ radialClosure s

theorem PiBase.subset_radialClosure {X : Type u} [TopologicalSpace X] (s : Set X) : s ⊆ radialClosure s

theorem PiBase.isRadiallyClosed_iff_radialClosure_eq {X : Type u} [TopologicalSpace X] (s : Set X) : IsRadiallyClosed s ↔ radialClosure s = s

theorem PiBase.ordinal_tendsto_closure {X : Type u} [TopologicalSpace X] {s : Set X} : radialClosure s ⊆ closure s

theorem PiBase.Denumerable.Set.univ (α : Type u) : Nonempty (Denumerable α) ↔ Nonempty (Denumerable ↑_root_.Set.univ)

A type α is denumerable iff univ : Set α is denumerable.

theorem PiBase.countable_equiv_type (α : Type u) [h : Countable α] : ∃ (ι : Type) (x : α ≃ ι), Countable ι

If α : Type u is countable, it is bijective to some countable r : Type.

@[instance_reducible]

noncomputable def PiBase.instSupSetFinOfNatNat_piBaseLean : SupSet (Fin 2)

Equations

• PiBase.instSupSetFinOfNatNat_piBaseLean = { sSup := fun (s : Set (Fin 2)) => if 1 ∈ s then 1 else 0 }

def PiBase.KAdditive {k : Cardinal.{u}} (f : Set ↑(Set.Iio k) → Fin 2) : Prop

Equations

• One or more equations did not get rendered due to their size.

def PiBase.IsMeasurable (k : Cardinal.{u}) : Prop

Equations

• One or more equations did not get rendered due to their size.