union — Mathlib

English

The union of two totally bounded sets is totally bounded (protected variant).

Русский

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

LaTeX

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

Lean4

/-- The union of two totally bounded sets is totally bounded. -/
protected theorem union {s t : Set α} (hs : TotallyBounded s) (ht : TotallyBounded t) : TotallyBounded (s ∪ t) :=
  totallyBounded_union.2 ⟨hs, ht⟩

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