isBounded_iUnion — Mathlib

English

If the index set is finite, the union over i of s(i) is bounded iff each s(i) is bounded.

Русский

Если индексный набор конечен, то объединение ⋃ i s(i) ограничено тогда и только тогда, когда каждый s(i) ограничен.

LaTeX

$$$\text{IsBounded}(\bigcup_i s(i)) \iff \forall i, \text{IsBounded}(s(i))$$$

Lean4

@[simp]
theorem isBounded_iUnion [Finite ι] {s : ι → Set α} : IsBounded (⋃ i, s i) ↔ ∀ i, IsBounded (s i) := by
  rw [← sUnion_range, isBounded_sUnion (finite_range s), forall_mem_range]

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