not_sbtw_self_right

Mathlib.Analysis.Convex.Between

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

English

No configuration can have Sbtw with the right and repeated positions; i.e., not Sbtw R x y y.

Русский

Никакая конфигурация не допускает Sbtw с повторяющимся правым концом; not Sbtw R x y y.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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