iUnion₂_mul — Mathlib

English

For s = (i ↦ κ i → Set α) and t ⊆ α, the product with a double-indexed union is subset of the double-indexed product: (⋃ 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

$$$(\\bigcap_{i,j} s_{i,j}) \\;*\\; t \\subseteq \\bigcap_{i,j} (s_{i,j} * t)$$$

Lean4

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

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