symm — Mathlib

English

If hr: ∀ a b, r₁₂ a b → r₂₁ b a then BiTotal r₁₂ → BiTotal r₂₁.

Русский

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

LaTeX

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

Lean4

protected theorem symm (hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) : BiTotal r₁₂ → BiTotal r₂₁ := fun h ↦
  ⟨h.2.symm hr, h.1.symm hr⟩

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