iUnion₂_div — Mathlib

English

Division distributes over a double union: ⋃ i, ⋃ j, s(i,j) / t = ⋃ i, ⋃ j, s(i,j) / t.

Русский

Деление распределяется по двойному объединению: ⋃ i, ⋃ j, s(i,j) / t = ⋃ i, ⋃ j, s(i,j) / t.

LaTeX

$$$$ \bigcup_i \bigcup_j (s(i,j) / t) = \bigcup_i \bigcup_j s(i,j) / t $$$$

Lean4

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

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