theorem PiBase.SeparationQuotient.isOpen_iff {X : Type u_1} [TopologicalSpace X] (s : Set X) : IsOpen s ↔ IsOpen (SeparationQuotient.mk '' s) ∧ SeparationQuotient.mk ⁻¹' SeparationQuotient.mk '' s = s

A set is open iff its image in the Kolmogorov quotient is open and saturated.

theorem PiBase.SeparationQuotient.isClosed_iff {X : Type u_1} [TopologicalSpace X] (s : Set X) : IsClosed s ↔ IsClosed (SeparationQuotient.mk '' s) ∧ SeparationQuotient.mk ⁻¹' SeparationQuotient.mk '' s = s

A set is clopen iff its image in the Kolmogorov quotient is open and saturated.

theorem PiBase.partitionTopology_iff_isOpen_iff_saturated (X : Type u) [TopologicalSpace X] : PartitionTopology X ↔ ∀ (s : Set X), IsOpen s ↔ SeparationQuotient.mk ⁻¹' SeparationQuotient.mk '' s = s

A space has partition topology iff every set is open iff it is saturated.

theorem PiBase.partitionTopology_iff_isClosed_iff_saturated (X : Type u) [TopologicalSpace X] : PartitionTopology X ↔ ∀ (s : Set X), IsClosed s ↔ SeparationQuotient.mk ⁻¹' SeparationQuotient.mk '' s = s

A space has partition topology iff every set is clopen iff it is saturated.

theorem PiBase.partitionTopology_iff_isOpen_iff_isClosed {X : Type u} [TopologicalSpace X] [h : PartitionTopology X] (s : Set X) : IsOpen s ↔ IsClosed s

theorem PiBase.PartitionTopology.inseparable_open (X : Type u) [TopologicalSpace X] [h : PartitionTopology X] (x : X) : IsOpen {y : X | Inseparable x y}

theorem PiBase.PartitionTopology.inseparable_closed (X : Type u) [TopologicalSpace X] [h : PartitionTopology X] (x : X) : IsClosed {y : X | Inseparable x y}

def PiBase.Formal.separationQuotientCongr {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) : SeparationQuotient X ≃ₜ SeparationQuotient Y

A homeomorphism φ : X ≃ₜ Y descends to a homeomorphism of the Kolmogorov quotients.

Equations

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

theorem PiBase.WellDefined.partitionTopology : WellDefined PartitionTopology