totallyBounded_insert — Mathlib

English

The union with a singleton preserves total boundedness: TotallyBounded(insert a s) iff TotallyBounded(s).

Русский

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

LaTeX

$$$$TotallyBounded(\\operatorname{insert}(a, s)) \\iff TotallyBounded(s).$$$$

Lean4

@[simp]
theorem totallyBounded_insert (a : α) {s : Set α} : TotallyBounded (insert a s) ↔ TotallyBounded s := by
  simp_rw [← singleton_union, totallyBounded_union, totallyBounded_singleton, true_and]

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