prodMk_snd — Mathlib

English

Two elements of a product are equal if their first and second projections agree.

Русский

Два элемента произведения равны, если их проекции по первым и вторым компонентам согласованы.

LaTeX

$$$ z.fst = w.fst \land z.snd = w.snd \Rightarrow z = w $$$

Lean4

@[simp]
theorem prodMk_snd {a : C} (x : F.obj a) (y : G.obj a) : (Limits.prod.snd (X := F)).app a (prodMk x y) = y := by
  simp only [prodMk, binaryProductIso_inv_comp_snd_apply]

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