comm_of — Mathlib

English

A version of commutativity with r explicit: r a b ↔ r b a.

Русский

Версия коммутативности с явным отношением: r a b ⇔ r b a.

LaTeX

$$$\\\\forall {a,b}, \\\\ r(a,b) \\\\leftrightarrow \\\\ r(b,a).$$$

Lean4

/-- A version of `comm` with `r` explicit.

This lemma matches the lemmas from lean core in `Init.Algebra.Classes`, but is missing there. -/
theorem comm_of (r : α → α → Prop) [IsSymm α r] {a b : α} : r a b ↔ r b a :=
  comm

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