biUnion_prod' — Mathlib

English

A distribution law for biUnion over a product: the biUnion over s and t of f(i,j) equals a double iUnion over i and j of f(i,j).

Русский

Закон распределения biUnion над произведением: biUnion по s и t равен двойному iUnion по i и j.

LaTeX

$$$\text{biUnion}~s~t ~f = \bigcup_{i\in s} \bigcup_{j\in t} f(i,j)$$$

Lean4

/-- Analogue of `biSup_prod` for sets. -/
theorem biUnion_prod' (s : Set β) (t : Set γ) (f : β × γ → Set α) : ⋃ x ∈ s ×ˢ t, f x = ⋃ (i ∈ s) (j ∈ t), f (i, j) :=
  biSup_prod

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