forall₂ — Mathlib

English

If R is BiUnique, then Forall₂ R is BiUnique: both left and right uniqueness carry over.

Русский

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

LaTeX

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

Lean4

theorem _root_.Relator.BiUnique.forall₂ (hr : BiUnique R) : BiUnique (Forall₂ R) :=
  ⟨hr.left.forall₂, hr.right.forall₂⟩

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