English
Let S be a set of sets and f a function from the base type to a complete lattice; the supremum over x in ⋃₀ S of f x equals the supremum over s in S and x in s of f x.
Русский
Пусть S — множество множеств и f — функция в полную решетку; верхняя граница по x в ⋃₀ S f(x) равна верхней границе по s∈S и x∈s f(x).
LaTeX
$$$\\big\\lceil \\;\\; \\text{iSup } x \\in \\bigcup_0 S f(x) = \\text{iSup}_{s \\in S} \\text{iSup}_{x \\in s} f(x) \\;\\rceil$$$
Lean4
theorem iSup_sUnion (S : Set (Set α)) (f : α → β) : (⨆ x ∈ ⋃₀ S, f x) = ⨆ (s ∈ S) (x ∈ s), f x := by
rw [sUnion_eq_iUnion, iSup_iUnion, ← iSup_subtype'']
