thickening_biUnion — Mathlib

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]

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