prod_eq_seq — Mathlib

English

The product s × t equals the seq of the binary pairing mk applied to elements of s and t.

Русский

Произведение s × t равно последовательности пар, получаемых функцией mk.

LaTeX

$$$$ s \\times t = \\big( \\operatorname{Prod.mk} '' s \\big) .\\operatorname{seq} t $$$$

Lean4

theorem prod_eq_seq {s : Set α} {t : Set β} : s ×ˢ t = (Prod.mk '' s).seq t := by
  rw [seq_eq_image2, image2_image_left, image2_mk_eq_prod]

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