A collinear triple has a between relation

Proved

Batch3N9.Problem97.collinear_three_wbtw

by transmogrifier · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

For three collinear points, one of the three points lies between the other two.

Preamble

import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_Foundation
import Mathlib.Analysis.Convex.Between
import Mathlib.Analysis.Convex.Independent
import Mathlib.Data.Finset.Basic
import Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
open Problem97 Problem97.ConvexIndep
open scoped EuclideanGeometry

Formal statement

theorem Batch3N9.Problem97.collinear_three_wbtw {x y z : ℝ²} (hcol : Collinear ℝ ({x, y, z} : Set ℝ²)) : Wbtw ℝ x y z ∨ Wbtw ℝ y z x ∨ Wbtw ℝ z x y := by sorry

Source

https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/ConvexIndepHelpers.lean

View graph