sSup_sUnion — Mathlib

English

For a collection s of sets, the supremum of the union of s equals the supremum over t in s of the supremum of t.

Русский

Для множества s множеств, верхняя граница объединения множества равна верхней границе для каждого элемента ∈ s.

LaTeX

$$$sSup(\\,\\bigcup s\\,) = \\bigvee_{t \\in s} sSup(t)$$$

Lean4

theorem sSup_sUnion (s : Set (Set β)) : sSup (⋃₀ s) = ⨆ t ∈ s, sSup t := by
  simp only [sUnion_eq_biUnion, sSup_eq_iSup, iSup_iUnion]

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