sbtw_pointReflection_of_ne

Mathlib.Analysis.Convex.Between

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

← MathLib Explorer

English

The triple (x, midpoint_R(x,y), y) is a betweenness configuration.

Русский

Тройка (x, midpoint_R(x,y), y) образует конфигурацию между.

LaTeX

$$$Wbtw_R x (midpoint_R x y) y$$$

Lean4

theorem sbtw_pointReflection_of_ne {x y : P} (h : x ≠ y) : Sbtw R y x (pointReflection R x y) :=
  by
  refine ⟨wbtw_pointReflection _ _ _, h, ?_⟩
  nth_rw 1 [← pointReflection_self R x]
  exact (pointReflection_involutive R x).injective.ne h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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