sUnion_bounded_univ — Mathlib

English

The union of all bounded subsets of α is the entire space, i.e., every point lies in some bounded set.

Русский

Объединение всех ограниченных подмножеств пространства α даёт всю площадь, то есть каждый элемент лежит в некотором ограниченном множества.

LaTeX

$$$\bigcup\{ S : Set(\,\alpha) \mid \text{IsBounded}(S) \} = \text{univ}$$$

Lean4

@[simp]
theorem sUnion_bounded_univ : ⋃₀ {s : Set α | IsBounded s} = univ :=
  sUnion_eq_univ_iff.2 fun a => ⟨{ a }, isBounded_singleton, mem_singleton a⟩

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