not_sbtw_self

Mathlib.Analysis.Convex.Between

URI: https://scilib.ai/kg/mathlib#not_sbtw_self

English

Similarly, not Sbtw R x y y holds for any x, y.

Русский

Аналогично, для любых x, y не выполняется Sbtw R x y y.

LaTeX

$$Not (Sbtw R x y y)$$

Lean4

@[simp]
theorem not_sbtw_self (x y : P) : ¬Sbtw R x y x := fun h => h.left_ne_right rfl

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

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

Разделы

Аффилиация

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