right_unique_forall₂' — Mathlib

English

If R is BiUnique, then Forall₂ R is BiUnique: left- and right-uniqueness lift to Forall₂.

Русский

Если R би-уникально, то Forall₂ R би-уникально: сохраняются левая и правая уникальность.

LaTeX

$$$ \text{If } \mathrm{BiUnique}\ R\ \Rightarrow\ \mathrm{BiUnique}\ (\mathrm{Forall₂}\ R) $$$

Lean4

theorem right_unique_forall₂' (hr : RightUnique R) : ∀ {a b c}, Forall₂ R a b → Forall₂ R a c → b = c
  | _, _, _, Forall₂.nil, Forall₂.nil => rfl
  | _, _, _, Forall₂.cons ha₀ h₀, Forall₂.cons ha₁ h₁ => hr ha₀ ha₁ ▸ right_unique_forall₂' hr h₀ h₁ ▸ rfl

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