closure_eq_lowerClosure — Mathlib

English

In this topology, the closure of a set equals its lower-closure.

Русский

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

LaTeX

$$$ \overline{s} = \mathrm{lowerClosure}(s).$$$

Lean4

theorem closure_eq_lowerClosure {s : Set α} : closure s = lowerClosure s :=
  by
  rw [subset_antisymm_iff]
  refine ⟨?_, lowerClosure_min subset_closure (isClosed_iff_isLower.1 isClosed_closure)⟩
  · apply closure_minimal subset_lowerClosure _
    rw [isClosed_iff_isLower]
    exact LowerSet.lower (lowerClosure s)

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