symm — Mathlib

English

If r₁₂ a b → r₂₁ b a holds and LeftTotal r₁₂, then RightTotal r₂₁.

Русский

Если для всех a,b из r₁₂ выполняется условие, что r₂₁ b a, и r₁₂ имеет левую полноту, то r₂₁ имеет правую полноту.

LaTeX

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

Lean4

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

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