ne_left

Mathlib.Analysis.Convex.Between

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

English

If x, y, z form a proper Sbtw triple, then the middle point y is not equal to the left endpoint x: y ≠ x.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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