prodMk_fst — Mathlib

English

Elements z and w of a product are equal iff their first components and second components are equal.

Русский

Элементы z и w произведения равны тогда и только тогда, когда их первые и вторые компоненты равны.

LaTeX

$$$ z = w \iff (z.1 = w.1) \land (z.2 = w.2) $$$

Lean4

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

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