English
The map PProd.mk is compatible with a basic elimination principle: given an equality (x1,y1)=(x2,y2), one can deduce any property that depends only on the coordinates x1=x2 and y1=y2 via a generic eliminator.
Русский
Функция PProd.mk согласуется с основным принципом устранения: если (x1,y1)=(x2,y2), то из свойств, зависящих только от координат, можно вывести произвольное утверждение.
LaTeX
$$$(x_1,y_1)=(x_2,y_2)\\;\\to\\;\\forall P\\;\\bigl((x_1=x_2 \\to y_1=y_2 \\to P) \\to P\\bigr).$$$
Lean4
def injArrow {α : Type*} {β : Type*} {x₁ : α} {y₁ : β} {x₂ : α} {y₂ : β} :
(x₁, y₁) = (x₂, y₂) → ∀ ⦃P : Sort*⦄, (x₁ = x₂ → y₁ = y₂ → P) → P := fun h₁ _ h₂ ↦ Prod.noConfusion h₁ h₂
