prod_ext — Mathlib

English

Extensionality principle for products: equality of the two projections implies equality of the whole element.

Русский

Принцип экстенсиональности для произведений: равенство первых компонентов означает равенство элементов.

LaTeX

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

Lean4

@[ext]
theorem prod_ext {a : C} (z w : (prod F G).obj a) (h1 : z.1 = w.1) (h2 : z.2 = w.2) : z = w :=
  Prod.ext h1 h2

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