totallyBounded_sUnion — Mathlib

English

A finite union (sUnion) of sets is totally bounded iff each member set is totally bounded.

Русский

Объединение по конечному множеству множеств (sUnion) полностью ограничено тогда и только тогда, когда каждый элемент множества полностью ограничен.

LaTeX

$$$$TotallyBounded(\\bigcup_0 S) \\iff \\forall s \\in S, TotallyBounded(s).$$$$

Lean4

/-- A union of a finite family of sets is totally bounded
if and only if each set of the family is totally bounded. -/
theorem totallyBounded_sUnion {S : Set (Set α)} (hS : S.Finite) : TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s :=
  by rw [sUnion_eq_biUnion, totallyBounded_biUnion hS]

Похожие утверждения