isClosed_upperClosure — Mathlib

English

The upper closure of a finite set is closed in the lower topology.

Русский

Верхнее замыкание конечного множества замкнуто в нижней топологии.

LaTeX

$$$\\text{If } s\\text{ is finite, then } \\operatorname{upperClosure}(s) \\text{ is closed in the lower topology.}$$$

Lean4

/-- The upper closure of a finite set is closed in the lower topology. -/
theorem isClosed_upperClosure (h : s.Finite) : IsClosed (upperClosure s : Set α) :=
  by
  simp only [← UpperSet.iInf_Ici, UpperSet.coe_iInf]
  exact h.isClosed_biUnion fun _ _ => isClosed_Ici

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