closure_singleton — Mathlib

English

In IsScott α univ, the closure of a singleton {a} is the left-closed ray {x | x ≤ a} (iic a).

Русский

В IsScott α univ замыкание множества {a} равно лучу слева {x | x ≤ a}.

LaTeX

$$$\\overline{\\{a\\}} = \\{x: x \\le a\\}$$$

Lean4

/-- The closure of a singleton `{a}` in the Scott topology is the right-closed left-infinite interval
`(-∞,a]`.
-/
@[simp]
theorem closure_singleton [IsScott α univ] : closure { a } = Iic a :=
  le_antisymm (closure_minimal (by rw [singleton_subset_iff, mem_Iic]) isClosed_Iic) <|
    by
    rw [← LowerSet.coe_Iic, ← lowerClosure_singleton]
    apply lowerClosure_subset_closure

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