sbtw_midpoint_of_ne — Mathlib

English

If x ≠ y, then y, x, and pointReflection_R(x,y) produce a betweenness configuration.

Русский

Если x ≠ y, то y, x и точечное отражение дают конфигурацию между.

LaTeX

$$$(\text{ne}) \Rightarrow Sbtw_R y x (pointReflection_R x y)$$$

Lean4

theorem sbtw_midpoint_of_ne {x y : P} (h : x ≠ y) : Sbtw R x (midpoint R x y) y :=
  by
  have h : midpoint R x y ≠ x := by simp [h]
  convert sbtw_pointReflection_of_ne R h
  rw [pointReflection_midpoint_left]

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