iUnion₂_smul — Mathlib

English

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

Русский

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

LaTeX

$$$$ \left( \bigcup_i \bigcup_j s(i,j) \right) \cdot t = \bigcup_i \bigcup_j (s(i,j) \cdot t) $$$$

Lean4

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

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