right_ne

Mathlib.Analysis.Convex.Between

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

English

Equivalently, the right endpoint z is not equal to the middle y: z ≠ y.

Русский

Аналогично, правый конец z не равен середине y: z ≠ y.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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