smul_iUnion₂ — Mathlib

English

The smul distributes over a double union on the right: s • ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s • t i j.

Русский

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

LaTeX

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

Lean4

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

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