closure_singleton — Mathlib

English

The closure of a singleton {a} in the lower topology is the left-closed right-infinite interval [a, ∞).

Русский

Замыкание множества {a} в нижней топологии равно интервалу [a, ∞).

LaTeX

$$$\\overline{\\{a\\}} = [a, \\infty)$ in the lower topology$$

Lean4

/-- The closure of a singleton `{a}` in the lower topology is the left-closed right-infinite interval
[a, ∞).
-/
@[simp]
theorem closure_singleton (a : α) : closure { a } = Ici a :=
  Subset.antisymm ((closure_minimal fun _ h => h.ge) <| isClosed_Ici) <|
    (isUpperSet_of_isClosed isClosed_closure).Ici_subset <| subset_closure rfl

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