hull_iSup — Mathlib

English

If α is a complete lattice and s is a function from an index set into α, then hull_T of the supremum of s equals the intersection of hull_T(s(i)) over all indices i.

Русский

Если α — полная решетка и s : ι → α, то оболочка hull_T над i–й верхней границей (iSup s) равна пересечению оболочек hull_T(s(i)) по всем i.

LaTeX

$$$\\mathrm{hull}(T, \\bigvee s) = \\bigcap_{i} \\mathrm{hull}(T, s(i)).$$$

Lean4

theorem hull_iSup {ι : Sort v} (s : ι → α) : hull T (iSup s) = ⋂ i, hull T (s i) := by aesop

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