div_iUnion₂ — Mathlib

English

Division distributes over a two-parameter union: s / ⋃ i, ⋃ j, t_i_j = ⋃ i, ⋃ j, s / t_i_j.

Русский

Деление над двойным объединением: s / ⋃ i, ⋃ j, t(i,j) = ⋃ i, ⋃ j, s / t(i,j).

LaTeX

$$$$ s / \bigcup_i \bigcup_j t_i_j = \bigcup_i \bigcup_j (s / t_i_j) $$$$

Lean4

@[to_additive]
theorem div_iUnion₂ (s : Set α) (t : ∀ i, κ i → Set α) : (s / ⋃ (i) (j), t i j) = ⋃ (i) (j), s / t i j :=
  image2_iUnion₂_right ..

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