iUnion_prod' — Mathlib

English

An analogue for iUnion over a product: the union over x ∈ β×γ of f x equals a double iUnion over i and j of f(i,j).

Русский

Аналогия для iUnion над произведением: объединение по x∈β×γ f(x) равно двойному iUnion по i и j f(i,j).

LaTeX

$$$\bigcup_{x \in \beta\times\gamma} f(x) = \bigcup_{i \in \beta} \bigcup_{j \in \gamma} f(i,j)$$$

Lean4

/-- Analogue of `iSup_prod` for sets. -/
theorem iUnion_prod' (f : β × γ → Set α) : ⋃ x : β × γ, f x = ⋃ (i : β) (j : γ), f (i, j) :=
  iSup_prod

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