symm — Mathlib

English

If hr: ∀ a b, r₁₂ a b → r₂₁ b a and RightTotal r₁₂ hold, then LeftTotal r₂₁ holds.

Русский

Если существует симметрия между r₁₂ и r₂₁, и правая полнота r₁₂, то левая полность r₂₁.

LaTeX

$$$ (\\forall a\\,b, r_{12} a b \\rightarrow r_{21} b a) \\rightarrow \\operatorname{RightTotal}(r_{12}) \\rightarrow \\operatorname{LeftTotal}(r_{21}) $$$

Lean4

protected theorem symm (hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) : RightTotal r₁₂ → LeftTotal r₂₁ :=
  LeftTotal.symm (fun _ _ ↦ hr _ _)

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