closure_singleton — Mathlib

English

In the upper topology, the closure of a singleton {a} is the left-infinite right-closed interval (-∞, a].

Русский

В верхней топологии замыкание множества вида {a} равно интервалу (-∞, a].

LaTeX

$$$\overline{\{a\}} = I\!I\!C(a)$$$

Lean4

/-- The closure of a singleton `{a}` in the upper topology is the left-infinite right-closed interval
(-∞,a].
-/
@[simp]
theorem closure_singleton (a : α) : closure { a } = Iic a :=
  IsLower.closure_singleton (α := αᵒᵈ) _

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