iUnion_prod — Mathlib

English

An equality exchanging iUnion and cartesian product holds: ⋃ x, s x × t x equals (⋃ x, s x) × (⋃ x, t x).

Русский

Справедливо равенство, меняющее iUnion и произведение: ⋃ x, s(x) × t(x) = (⋃ x, s(x)) × (⋃ x, t(x)).

LaTeX

$$$\bigcup_{x} (s_x \times t_x) = (\bigcup_x s_x) \times (\bigcup_x t_x)$$$

Lean4

theorem iUnion_prod {ι ι' α β} (s : ι → Set α) (t : ι' → Set β) :
    ⋃ x : ι × ι', s x.1 ×ˢ t x.2 = (⋃ i : ι, s i) ×ˢ ⋃ i : ι', t i :=
  by
  ext
  simp

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