forall₂ — Mathlib

English

If R is RightUnique, then Forall₂ R is RightUnique: the right component is determined by the left one and R.

Русский

Если R — правая уникальность, то Forall₂ R также правая уникальность: правая часть определяется левой и R.

LaTeX

$$$ \text{Relator.RightUnique.forall₂ }(hr) :\text{ RightUnique }(\mathrm{Forall₂ R}) $$$

Lean4

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

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