map_def — Mathlib

English

Let f: α → γ and g: β → δ. The product map sends (a,b) to (f(a), g(b)).

Русский

Пусть f: α → γ и g: β → δ. Отображение произведения переводит (a,b) в (f(a), g(b)).

LaTeX

$$$\\\\operatorname{Prod.map} f g = \\\\lambda p:\\\\alpha \\\\times \\\\beta \\\\mapsto (f(p.1), g(p.2)).$$$

Lean4

theorem map_def {f : α → γ} {g : β → δ} : Prod.map f g = fun p : α × β ↦ (f p.1, g p.2) :=
  funext fun p ↦ Prod.ext (map_fst f g p) (map_snd f g p)

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