ne_right

Mathlib.Analysis.Convex.Between

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

English

In a proper Sbtw triple, the middle element y is not equal to the right endpoint z: y ≠ z.

Русский

В допустимом тройном Sbtw середина y не равна правому концу z: y ≠ z.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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