thickening_union — Mathlib

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]

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