English
For a family of sets f i and a subset I, thickening distributes over the biUnion: thickening δ (⋃ i ∈ I, f i) = ⋃ i ∈ I, thickening δ (f i).
Русский
Для семейства множеств f i и подмножества I утолщение распределяется по биобъединению: thickening δ (⋃ i ∈ I, f i) = ⋃ i ∈ I, thickening δ (f i).
LaTeX
$$$\\mathrm{thickening}_{\\delta}\\Bigl(\\bigcup_{i \\in I} f(i)\\Bigr) = \\bigcup_{i \\in I} \\mathrm{thickening}_{\\delta}(f(i)).$$$
Lean4
theorem thickening_biUnion {ι : Type*} (δ : ℝ) (f : ι → Set α) (I : Set ι) :
thickening δ (⋃ i ∈ I, f i) = ⋃ i ∈ I, thickening δ (f i) := by simp only [thickening_iUnion]