English
If I is finite and each S(i) is bounded below, then the union ⋃_{i∈I} S(i) is bounded below; conversely, if the union is bounded below, every S(i) is bounded below.
Русский
Если множество индексов I конечное и каждый S(i) имеет нижнюю границу, то объединение ⋃_{i∈I} S(i) также имеет нижнюю границу; наоборот, если ⋃_{i∈I} S(i) ограничено снизу, тогда каждый S(i) ограничен снизу.
LaTeX
$$$BddBelow\\left(\\bigcup_{i \\in I} S(i)\\right) \\iff \\forall i \\in I, BddBelow\\left(S(i)\\right)$$$
Lean4
/-- A finite union of sets which are all bounded below is still bounded below. -/
theorem bddBelow_biUnion {I : Set β} {S : β → Set α} (H : I.Finite) :
BddBelow (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddBelow (S i) :=
Finite.bddAbove_biUnion (α := αᵒᵈ) H
