theorem PiBase.TopologicalSpace.indiscrete_iff_isOpen_iff_empty_or_univ (X : Type u) [TopologicalSpace X] : IndiscreteTopology X ↔ ∀ (U : Set X), IsOpen U ↔ U = ∅ ∨ U = Set.univ

A space is indiscrete iff all open sets are either the empty space or the entire space.

@[simp]

theorem PiBase.TopologicalSpace.le_top (X : Type u) [τ : TopologicalSpace X] : τ ≤ ⊤

Every topological space is as least as fine as the indiscrete topology.

@[simp]

theorem PiBase.TopologicalSpace.bot_le (X : Type u) [τ : TopologicalSpace X] : ⊥ ≤ τ

Every topological space is as least as coarse as the indiscrete topology.

theorem PiBase.Homeomorph.indiscreteTopology {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [h : IndiscreteTopology X] (f : X ≃ₜ Y) : IndiscreteTopology Y

theorem PiBase.WellDefined.indiscreteTopology : WellDefined IndiscreteTopology