isBounded_sUnion — Mathlib

English

For a finite S of subsets, the union ⋃₀ S is bounded iff every member s ∈ S is bounded.

Русский

Для конечного S: объединение ⋃₀ S ограничено тогда и только тогда, когда каждый элемент s ∈ S ограничен.

LaTeX

$$$\text{IsBounded}(\bigcup\_{S \in \mathcal{S}} S) \iff \forall S \in \mathcal{S}, \text{IsBounded}(S)$$$

Lean4

theorem isBounded_sUnion {S : Set (Set α)} (hs : S.Finite) : IsBounded (⋃₀ S) ↔ ∀ s ∈ S, IsBounded s := by
  rw [sUnion_eq_biUnion, isBounded_biUnion hs]

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