left_unique_forall₂' — Mathlib

English

If R is LeftUnique, then Forall₂ R lifts left-uniqueness: for any lists a, b, c, if Forall₂ R a c and Forall₂ R b c, then a = b.

Русский

Пусть R — отношение с левой уникальностью. Тогда если Forall₂ R a c и Forall₂ R b c, то a = b.

LaTeX

$$$ \text{If } \mathrm{LeftUnique}\ R,\ \forall a\,b\,c:\ \mathrm{List}\,\alpha,\ \mathrm{Forall₂}\ R\ a\ c\ \to\ \mathrm{Forall₂}\ R\ b\ c\ \to\ a=b $$$

Lean4

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

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