forall₂ — Mathlib

English

If R is RightUnique, then Forall₂ R is RightUnique: if Forall₂ R a b and Forall₂ R a c then b = c.

Русский

Пусть R — правая уникальность. Тогда Forall₂ R также имеет правую уникальность: если Forall₂ R a b и Forall₂ R a c, то b = c.

LaTeX

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

Lean4

theorem _root_.Relator.LeftUnique.forall₂ (hr : LeftUnique R) : LeftUnique (Forall₂ R) :=
  @left_unique_forall₂' _ _ _ hr

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