prodEquiv_apply_snd — Mathlib

English

Let X1 and X2 be objects with a binary product X1 ⨯ X2. The canonical isomorphism between the product in the category and the cartesian product of the underlying objects preserves the second projection: for every input x, snd(prodEquiv X1 X2 x) equals the cartesian second projection applied to x.

Русский

Пусть X1 и X2 имеют бинарный произведение X1 ⨯ X2. Каноническое изоморфизм между произведением и каркассианным произведением сохраняет вторую проекцию: для каждого элемента x выполняется snd(prodEquiv X1 X2 x) = (Limits.prod.snd) x.

LaTeX

$$$\\\\operatorname{snd}(\\\\mathrm{prodEquiv}\\\\, X_1 \\, X_2 \\, x) = (\\\\mathrm{Limits.prod.snd} : X_1 \\times X_2 \\to X_2) \\, x$$$

Lean4

@[simp]
theorem prodEquiv_apply_snd (x : ToType (X₁ ⨯ X₂)) : (prodEquiv X₁ X₂ x).snd = (Limits.prod.snd : X₁ ⨯ X₂ ⟶ X₂) x :=
  congr_fun (prodComparison_snd (forget C) X₁ X₂) x

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