English
A finite union of sets each bounded above is bounded above; equivalently, the union is bounded above iff each member is bounded above.
Русский
Конъюнкция конечного объединения множест̆в, каждое из которых ограничено сверху, также ограничена сверху; эквивалентно, что объединение ограничено сверху тогда и только тогда, когда каждый элемент ограничен сверху.
LaTeX
$$$I\text{ finite} \Rightarrow BddAbove(\bigcup_{i\in I} S_i) \iff \forall i\in I, BddAbove(S_i).$$$
Lean4
/-- A finite union of sets which are all bounded above is still bounded above. -/
theorem bddAbove_biUnion {I : Set β} {S : β → Set α} (H : I.Finite) :
BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i) := by
induction I, H using Set.Finite.induction_on with
| empty => simp only [biUnion_empty, bddAbove_empty, forall_mem_empty]
| insert _ _ hs => simp only [biUnion_insert, forall_mem_insert, bddAbove_union, hs]
