English
A union over a finite index set I of sets s_i is totally bounded iff every s_i with i ∈ I is totally bounded.
Русский
Объединение по конечному подмножеству индексов I: ⋃_{i∈I} s_i полностью ограничено тогда и только тогда, когда каждый s_i с i∈I полностью ограничен.
LaTeX
$$$$TotallyBounded\\Big(\\bigcup_{i\\in I} s_i\\Big) \\iff \\forall i\\in I, TotallyBounded(s_i).$$$$
Lean4
/-- A union indexed by a finite set is totally bounded
if and only if each set of the family is totally bounded. -/
theorem totallyBounded_biUnion {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set α} :
TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i) :=
by
have := hI.to_subtype
rw [biUnion_eq_iUnion, totallyBounded_iUnion, Subtype.forall]
