eq_bot_or_top — Mathlib

English

In a space with the indiscrete topology, every open subset is either empty or the whole space.

Русский

В пространстве с индиcкретной топологией любая открытая подмножество либо пустая, либо равна всему пространству.

LaTeX

$$$\forall U \in \operatorname{Opens}(\alpha),\ U = \varnothing \ \lor\ U = \alpha$$$

Lean4

/-- An open set in the indiscrete topology is either empty or the whole space. -/
theorem eq_bot_or_top {α} [t : TopologicalSpace α] (h : t = ⊤) (U : Opens α) : U = ⊥ ∨ U = ⊤ :=
  by
  subst h; letI : TopologicalSpace α := ⊤
  rw [← coe_eq_empty, ← coe_eq_univ, ← isOpen_top_iff]
  exact U.2

Похожие утверждения