Bisection_of_Straight_Line
Provedlinesproofwiki
It is possible to bisect a straight line segment.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Bisection_of_Straight_Line (a b : ℝ) : ∃ m : ℝ, m = (a + b) / 2 ∧ |m - a| = |m - b| := by sorry
Source