rel_flip — Mathlib

English

For any relation r, Rel (flip r) s t holds if and only if Rel r t s holds. In words, reversing the order of the arguments in the relation flips the direction of the relation.

Русский

Для любой связи r, Rel (flip r) s t выполняется тогда и только тогда, когда Rel r t s выполняется. Иными словами, обращение порядка аргументов в отношении разворачивает направление отношения.

LaTeX

$$$Rel(\text{flip } r)\ s\ t \iff Rel(r)\ t\ s$$$

Lean4

theorem rel_flip {s t} : Rel (flip r) s t ↔ Rel r t s :=
  ⟨rel_flip_aux, rel_flip_aux⟩

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