prod_eq_biUnion_right — Mathlib

English

Let s ⊆ α and t ⊆ β. Then the cartesian product s × t equals the union over b ∈ t of the set { (a,b) | a ∈ s }.

Русский

Пусть s ⊆ α и t ⊆ β. Тогда множество s × t равно объединению по b ∈ t множества { (a,b) | a ∈ s }.

LaTeX

$$$$ s \\times t = \\bigcup_{b \\in t} \\{ (a,b) \\mid a \\in s \\} $$$$

Lean4

theorem prod_eq_biUnion_right : s ×ˢ t = ⋃ b ∈ t, (fun a => (a, b)) '' s := by
  rw [iUnion_image_right, image2_mk_eq_prod]

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