This file contains additional "meta" definitions and statemtns about topological properties which are useful for properties and theorems.

@[reducible, inline]

abbrev PiBase.IsHomeo (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] : Prop

A proposition for two spaces being homeomorphic.

Equations

• PiBase.IsHomeo X Y = Nonempty (X ≃ₜ Y)

theorem PiBase.Homeomorph.isHomeo {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) : IsHomeo X Y

If there is a homeomorphism between two spaces, then they are homeomorph.

theorem PiBase.IsHomeo.refl {X : Type u_1} [TopologicalSpace X] : IsHomeo X X

Every space is homeomorph to itself.

theorem PiBase.IsHomeo.symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : IsHomeo X Y) : IsHomeo Y X

If X is homeomorph to Y, Y is homeomorph to `X´.

theorem PiBase.IsHomeo.trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (xy : IsHomeo X Y) (yz : IsHomeo Y Z) : IsHomeo X Z

If X is homeomorph to Y and Y´ is homeomorph to Z, then Xis homeomorph toZ`.

theorem PiBase.IsHomeo.Set.univ (X : Type u) [TopologicalSpace X] : IsHomeo (↑_root_.Set.univ) X

A space X is homeomorph to univ : Set X.

theorem PiBase.IsHomeo.funUnique (ι : Type u_4) (X : Type u_5) [Unique ι] [TopologicalSpace X] : IsHomeo (ι → X) X

theorem PiBase.IsHomeo.subset_preimage {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y) (s : Set Y) : IsHomeo ↑(⇑f ⁻¹' s) ↑s

theorem PiBase.IsHomeo.piCongrRight {ι : Type u_4} {Y₁ Y₂ : ι → Type u} [(i : ι) → TopologicalSpace (Y₁ i)] [(i : ι) → TopologicalSpace (Y₂ i)] (F : (i : ι) → Y₁ i ≃ₜ Y₂ i) : IsHomeo ((i : ι) → Y₁ i) ((i : ι) → Y₂ i)

@[reducible, inline]

abbrev PiBase.WellDefined (P : (X : Type u) → [TopologicalSpace X] → Prop) : Prop

We say a property of topological spaces is well-defined, if it is preserved by homeomorphisms.

Note: This suffers from universe issues, so it should not be used in isolation. However it is strong enough to prove some "meta"-theorems, i.e. Hereditary => Property (see below)

A proof that some property Ex (defined on all universes, which is almost always the case) is well-defined should first have that Ex is preserved by homeomorphisms over arbitrary universes (which we can not properly quantify), i.e. a theorem Homeomorph.ex. Then proving that Ex is well-defined can always be done in the following way:

theorem WellDefined.ex : WellDefined Ex :=
  fun {_ _} _ _ h _ ↦ Homeomorph.ex h.some

Equations

• PiBase.WellDefined P = ∀ {X Y : Type ?u.1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], PiBase.IsHomeo X Y → P X → P Y

theorem PiBase.WellDefined.homeo {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {P : (X : Type u) → [TopologicalSpace X] → Prop} (h : WellDefined P) (f : X ≃ₜ Y) (hX : P X) : P Y

theorem PiBase.WellDefined.Set.univ {P : (X : Type u) → [TopologicalSpace X] → Prop} (hP : WellDefined P) {X : Type u} [TopologicalSpace X] : P X ↔ P ↑_root_.Set.univ

A well defined property P holds for X iff it holds for univ : Set X.

def PiBase.Sigma {X : Type v} [TopologicalSpace X] (P : {α : Type u} → (α → Set X) → Prop) {ι : Type u} (f : ι → Set X) : Prop

A collection of sets which is the countable union of collection of sets which have some property. (I.e. sigma locally finite)

Equations

• PiBase.Sigma P f = ∃ (ω : Type ?u.2) (r : ω → Set ι), Countable ω ∧ ⋃ (i : ω), r i = Set.univ ∧ ∀ (i : ω), P fun (j : ↑(r i)) => f ↑j

theorem PiBase.property_to_sigma {X : Type u_1} [TopologicalSpace X] {P : {α : Type u} → (α → Set X) → Prop} (hP : ∀ {α β : Type u} (l : α → Set X) (e : β ≃ α), P l → P (l ∘ ⇑e)) {ι : Type u} {f : ι → Set X} (h : P f) : Sigma (fun {α : Type u} => P) f

A collection of sets with a well defined property also has the sigma version of the property.

def PiBase.Omega (P : (Y : Type u) → [TopologicalSpace Y] → Prop) (X : Type u) [TopologicalSpace X] : Prop

For a property P on topological spaces, we say Omega P, is every power of a space satisfies P

Equations

• PiBase.Omega P X = ∀ (n : ℕ), P (Fin n → X)

@[instance_reducible]

instance PiBase.instTopologicalSpaceOfIsEmpty (α : Type u) [IsEmpty α] : TopologicalSpace α

A empty set is a topological space (with a unique topology).

Equations

• PiBase.instTopologicalSpaceOfIsEmpty α = { IsOpen := fun (x : Set α) => True, isOpen_univ := trivial, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

theorem PiBase.Omega.toProperty {Z : Type u} [TopologicalSpace Z] {P : (X : Type u) → [TopologicalSpace X] → Prop} (hP : WellDefined P) (hZ : Omega P Z) : P Z

If Omega P X holds, then P X holds for well defined properties P.

theorem PiBase.Omega.wellDefined {P : (X : Type u) → [TopologicalSpace X] → Prop} (h : WellDefined P) : WellDefined (Omega P)

If P is a well-defined property, Omega P is as well. Note this is likely not too useful in practice, as we wants to prove the stronger version that Omega P is preserved by homeomorphisms.

theorem PiBase.Omega.toUnique {P : (X : Type u) → [TopologicalSpace X] → Prop} {Z X : Type u} [TopologicalSpace Z] [Unique X] [TopologicalSpace X] (h : WellDefined P) (hZ : Omega P Z) : P X

theorem PiBase.omega_of_imp {Z : Type u} [TopologicalSpace Z] {P Q : (X : Type u) → [TopologicalSpace X] → Prop} (h : ∀ (X : Type u) (x : TopologicalSpace X), P X → Q X) (hP : Omega P Z) : Omega Q Z

If P => Q, then Omega P => Omega Q.

def PiBase.Hereditarily (P : (Y : Type u) → [TopologicalSpace Y] → Prop) (X : Type u) [TopologicalSpace X] : Prop

For a property P of topological spaces, Hereditarily P means P holds for all subspaces.

Equations

• PiBase.Hereditarily P X = ∀ (s : Set X), P ↑s

theorem PiBase.Hereditarily.wellDefined {P : (X : Type u) → [TopologicalSpace X] → Prop} (h : WellDefined P) : WellDefined (Hereditarily P)

If P is a well-defined property, Hereditarily P is as well. Note this is likely not too useful in practice, as we wants to prove the stronger version that Hereditarily P is preserved by homeomorphisms.

theorem PiBase.Hereditarily.hereditarily {Z : Type u} [TopologicalSpace Z] {P : (X : Type u) → [TopologicalSpace X] → Prop} (h : WellDefined P) (hX : Hereditarily (Hereditarily P) Z) : Hereditarily P Z

theorem PiBase.Hereditarily.implies {Z : Type u} [TopologicalSpace Z] {P Q : (X : Type u) → [TopologicalSpace X] → Prop} (h : ∀ (X : Type u) (x : TopologicalSpace X), P X → Q X) (hZ : Hereditarily P Z) : Hereditarily Q Z

theorem PiBase.Hereditarily.toProperty {Z : Type u} [TopologicalSpace Z] {P : (X : Type u) → [TopologicalSpace X] → Prop} (hP : WellDefined P) (hZ : Hereditarily P Z) : P Z

For a well defined property P, Hereditarily P X implies P X

def PiBase.Locally (P : (Y : Type u) → [TopologicalSpace Y] → Prop) (X : Type u) [TopologicalSpace X] : Prop

For a property P, Locally P means every point has a neighborhood basis satisfying P. Note: Usage of Locally is sometimes inconsistent in the π-base.

Equations

• PiBase.Locally P X = ∀ (x : X), (nhds x).HasBasis (fun (s : Set X) => s ∈ nhds x ∧ P ↑s) id

def PiBase.WeaklyLocally (P : (Y : Type u) → [TopologicalSpace Y] → Prop) (X : Type u) [TopologicalSpace X] : Prop

For a property P, WeaklyLocally P means every point has a neighborhood satisfying P. Note: Usage of WeaklyLocally is sometimes inconsistent in the π-base.

Equations

• PiBase.WeaklyLocally P X = ∀ (x : X), ∃ s ∈ nhds x, P ↑s

theorem PiBase.Locally.weaklyLocally {Z : Type u} [TopologicalSpace Z] {P : (X : Type u) → [TopologicalSpace X] → Prop} (hZ : Locally P Z) : WeaklyLocally P Z

Locally P implies WeaklyLocally P.

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

Equations

• PiBase.IsPiBase s = (∅ ∉ s ∧ (∀ a ∈ s, IsOpen a) ∧ ∀ (o : Set X), IsOpen o → o.Nonempty → ∃ t ∈ s, t ⊆ o)