biUnion_prod — Mathlib

English

The image under a function of a biUnion over a product equals a nested iUnion of images over the product indices.

Русский

Образ под функцией биобъединения над произведением равен вложенному iUnion образов по индексам.

LaTeX

$$$\bigcup_{x \in s \times t} f(x) = \bigcup_{i \in s} \bigcup_{j \in t} f(i,j)$$$

Lean4

theorem biUnion_prod {α β γ} (s : Set α) (t : Set β) (f : α → Set γ) (g : β → Set δ) :
    ⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 = (⋃ x ∈ s, f x) ×ˢ (⋃ x ∈ t, g x) :=
  by
  ext ⟨_, _⟩
  simp only [mem_iUnion, mem_prod, exists_prop, Prod.exists]; tauto

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