left_ne_right_of_ne_left — Mathlib

English

If Wbtw holds for two different placements and certain non-equality holds, then the left endpoint must be distinct from the right endpoint; i.e., left_ne_right_of_ne_left.

Русский

Если выполняются условия Wbtw и неравенство, то левый конец отличается от правого.

LaTeX

$$Wbtw R x y z → Ne y x → Ne x z$$

Lean4

theorem left_ne_right_of_ne_left {x y z : P} (h : Wbtw R x y z) (hne : y ≠ x) : x ≠ z :=
  by
  rintro rfl
  rw [wbtw_self_iff] at h
  exact hne h

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