thickening_iUnion — Mathlib

English

The thickening commutes with arbitrary unions: thickening δ (⋃ i, f i) = ⋃ i, thickening δ (f i).

Русский

Утолщение бюлль по произвольным объединениям: thickening δ (⋃ i, f i) = ⋃ i, thickening δ (f i).

LaTeX

$$$\\mathrm{thickening}_{\\delta}\\left(\\bigcup_i f(i)\\right) = \\bigcup_i \\mathrm{thickening}_{\\delta}(f(i)).$$$

Lean4

@[simp]
theorem thickening_iUnion (δ : ℝ) (f : ι → Set α) : thickening δ (⋃ i, f i) = ⋃ i, thickening δ (f i) := by
  simp_rw [thickening, infEdist_iUnion, iInf_lt_iff, setOf_exists]

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