left_ne

Mathlib.Analysis.Convex.Between

URI: https://scilib.ai/kg/mathlib#Sbtw.left_ne

English

From Sbtw, it follows that x ≠ y for the left pair: the left endpoint is not equal to the middle point.

Русский

Из Sbtw следует, что x ≠ y для пары слева: левый конец не равен середине.

LaTeX

$$$Sbtw R x y z \Rightarrow x \neq y$$$

Lean4

theorem left_ne {x y z : P} (h : Sbtw R x y z) : x ≠ y :=
  h.2.1.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru