closure_singleton — Mathlib

English

The closure of a singleton {a} in the lower-set topology is the ray Ici a (all elements ≥ a).

Русский

Замыкание множества {a} в топологии нижних множеств равно интервалу Ici a (≤ a).

LaTeX

$$$$ \\mathrm{closure}\\bigl(\\{a\\}\\bigr) = \\mathrm{Ici}(a). $$$$

Lean4

/-- The closure of a singleton `{a}` in the lower set topology is the right-closed left-infinite
interval (-∞,a].
-/
@[simp]
theorem closure_singleton {a : α} : closure { a } = Ici a :=
  by
  rw [closure_eq_upperClosure, upperClosure_singleton]
  rfl

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