closure_eq_upperClosure — Mathlib

English

The closure of a set s in the lower-set topology equals its upper closure when viewed under duality.

Русский

Замыкание множества s в топологии нижних множеств равно его верхнему замыканию через дуальность.

LaTeX

$$$$ \\mathrm{closure}(s) = \\operatorname{upperClosure}(s). $$$$

Lean4

theorem closure_eq_upperClosure {s : Set α} : closure s = upperClosure s :=
  IsUpperSet.closure_eq_lowerClosure (α := αᵒᵈ)

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