right_iff_left_not_left — Mathlib

English

In a nonstrict strict order, an element is related in the right direction exactly when it is related on the left and not on the reverse.

Русский

В нестрогом строгом порядке связь направлена вправо тогда и только тогда, когда она существует слева и не существует справа.

LaTeX

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

Lean4

theorem right_iff_left_not_left {r s : α → α → Prop} [IsNonstrictStrictOrder α r s] {a b : α} :
    s a b ↔ r a b ∧ ¬r b a :=
  IsNonstrictStrictOrder.right_iff_left_not_left _ _

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