right_iff_left_not_left_of — Mathlib

English

A variant of the previous relation equivalence with explicit r and s: s a b holds iff r a b and not r b a.

Русский

Вариант предыдущего тождества относительно явных $r$ и $s$: $s\,a\,b$ эквивалентно $r\,a\,b$ и не $r\,b\,a$.

LaTeX

$$s a b ↔ r a b ∧ ¬ r b a$$

Lean4

/-- A version of `right_iff_left_not_left` with explicit `r` and `s`. -/
theorem right_iff_left_not_left_of (r s : α → α → Prop) [IsNonstrictStrictOrder α r s] {a b : α} :
    s a b ↔ r a b ∧ ¬r b a :=
  right_iff_left_not_left

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