isBounded_biUnion — Mathlib

English

For a finite set s of indices and f i, the union ⋃ i∈s f i is bounded iff each f i is bounded.

Русский

Для конечного множества индексов s: ограничено ли объединение ⋃ i∈s f i эквивалентно тому, что каждый f i ограничен.

LaTeX

$$$\text{IsBounded}(\bigcup_{i∈s} f(i)) \iff \forall i∈s, \text{IsBounded}(f(i))$$$

Lean4

theorem isBounded_biUnion {s : Set ι} {f : ι → Set α} (hs : s.Finite) :
    IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, IsBounded (f i) := by
  simp only [← isCobounded_compl_iff, compl_iUnion, isCobounded_biInter hs]

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