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]