product_eq_biUnion_right — Mathlib

English

The cartesian product s ×ˢ t equals the right-biUnion of t with images of s under pairing.

Русский

Декартово произведение s ×ˢ t равно правой биобъединению по t с отображением пары.

LaTeX

$$$s \timesˢ t = t.biUnion \bigl( \lambda b: s.image (\lambda a: (a,b)) \bigr)$$$

Lean4

theorem product_eq_biUnion_right [DecidableEq (α × β)] (s : Finset α) (t : Finset β) :
    s ×ˢ t = t.biUnion fun b => s.image fun a => (a, b) := by grind

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