totallyBounded_union — Mathlib

English

The union of two totally bounded sets is totally bounded.

Русский

Объединение двух полностью ограниченных множеств полностью ограничено.

LaTeX

$$$$TotallyBounded(s \\cup t) \\iff TotallyBounded(s) \\land TotallyBounded(t).$$$$

Lean4

/-- The union of two sets is totally bounded
if and only if each of the two sets is totally bounded. -/
@[simp]
theorem totallyBounded_union {s t : Set α} : TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t :=
  by
  rw [union_eq_iUnion, totallyBounded_iUnion]
  simp [and_comm]

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