cthickening_union — Mathlib

English

Closed thickening also distributes over union: cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t.

Русский

Закрытое утолщение распределяется по объединению: cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t.

LaTeX

$$$\\mathrm{cthickening}_{\\delta}(s \\cup t) = \\mathrm{cthickening}_{\\delta}(s) \\cup \\mathrm{cthickening}_{\\delta}(t).$$$

Lean4

@[simp]
theorem cthickening_union (δ : ℝ) (s t : Set α) : cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t := by
  simp_rw [cthickening, infEdist_union, min_le_iff, setOf_or]

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