hull_sSup — Mathlib

English

For any set S in a complete lattice α, hull_T(sSup S) equals the intersection of hull_T(a) over all a in S.

Русский

Для множества S в полной решетке α оболочка hull_T над sSup S равна пересечению hull_T(a) по всем a в S.

LaTeX

$$$\\mathrm{hull}(T, \\sup S) = \\bigcap_{a\\in S} \\mathrm{hull}(T, a).$$$

Lean4

theorem hull_sSup (S : Set α) : hull T (sSup S) = ⋂₀ {hull T a | a ∈ S} := by
  aesop
    /- When `α` is complete, a set is Lower topology relative-open if and only if it is of the form
    `(hull T a)ᶜ` for some `a` in `α`.-/

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