map_mk — Mathlib

English

Mapping a pair x = (a,b) with f yields (f a, f b). In symbols, Sym2.map f (Sym2.mk x) = Sym2.mk (Prod.map f f x).

Русский

Отображение пары x=(a,b) функцией f дает пару (f a, f b). То есть Sym2.map f (Sym2.mk x) = Sym2.mk (Prod.map f f x).

LaTeX

$$$ \\operatorname{Sym2.map} f\\; (\\operatorname{Sym2.mk} x) = \\operatorname{Sym2.mk} (\\operatorname{Prod.map} f f x). $$$

Lean4

theorem map_mk (f : α → β) (x : α × α) : map f (Sym2.mk x) = Sym2.mk (Prod.map f f x) :=
  rfl

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