English
Let u : ι → α and suppose each u_i is the least upper bound of s_i, i.e., IsLUB(s_i, u_i) for all i. Then for any c ∈ α, IsLUB{Set.range(u)}(c) holds iff IsLUB(⋃_i s_i)(c).
Русский
Пусть u : ι → α и для каждого i выполняется IsLUB(s_i, u_i). Тогда для любого c ∈ α: IsLUB( Set.range(u) , c ) эквивалентно IsLUB( ⋃_i s_i , c ).
LaTeX
$$$\\left( \\forall i, \\IsLUB(s_i, u_i) \\right) \\to \\left( \\IsLUB(\\operatorname{range}(u), c) \\iff \\IsLUB\\left(\\bigcup_i s_i\\right, c) \\right).$$$
Lean4
theorem isLUB_iUnion_iff_of_isLUB {u : ι → α} (hs : ∀ i, IsLUB (s i) (u i)) (c : α) :
IsLUB (Set.range u) c ↔ IsLUB (⋃ i, s i) c :=
by
refine isLUB_congr ?_
simp_rw [range_eq_iUnion, upperBounds_iUnion, upperBounds_singleton, (hs _).upperBounds_eq]
