sSup_iUnion — Mathlib

English

For a family t: ι → Set β in a complete lattice, the supremum of the union ⋃ i, t i equals the supremum over i of the supremum of t i.

Русский

Для семейства t: ι → Set β в полной решетке, верхняя граница объединения равна верхней границе и для каждого i верхняя граница t i.

LaTeX

$$$sSup(\\bigcup_i t_i) = \\bigvee_i sSup(t_i)$$$

Lean4

theorem sSup_iUnion (t : ι → Set β) : sSup (⋃ i, t i) = ⨆ i, sSup (t i) := by simp_rw [sSup_eq_iSup, iSup_iUnion]

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