English
The thickening distributes over union: thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t.
Русский
Утолщение распределяется по объединению: thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t.
LaTeX
$$$\\mathrm{thickening}_{\\delta}(s \\cup t) = \\mathrm{thickening}_{\\delta}(s) \\cup \\mathrm{thickening}_{\\delta}(t).$$$
Lean4
@[simp]
theorem thickening_union (δ : ℝ) (s t : Set α) : thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t := by
simp_rw [thickening, infEdist_union, min_lt_iff, setOf_or]