cthickening_empty — Mathlib

English

The closed thickening of the empty set is empty: cthickening δ ∅ = ∅.

Русский

Закрытое утолщение пустого множества равно пустому множеству: cthickening δ ∅ = ∅.

LaTeX

$$$ cthickening δ (\emptyset) = \emptyset $$$

Lean4

/-- The closed thickening of the empty set is empty. -/
@[simp]
theorem cthickening_empty (δ : ℝ) : cthickening δ (∅ : Set α) = ∅ := by
  simp only [cthickening, ENNReal.ofReal_ne_top, setOf_false, infEdist_empty, top_le_iff]

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