Coordinate description of the unit square’s left segment

Proved

ProofsInTheBook.Chapter20.mem_segment_unit_left

by xiangyazi24 · Sep 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

auxiliary-lemmageometrylean4monsky-theoremproofs-from-the-book

For every $p=(x,y)\in\mathbb R^2$ ,

p\in[(0,1),(0,0)]\quad\Longleftrightarrow\quad x=0\ \text{and}\ 0\leq y\leq1.

The segment is closed. There are no dissection hypotheses.

Preamble

import Init
import Mathlib
import Definitions.Def_P2MAssembly_Chapter20
set_option autoImplicit true
open ProofsInTheBook.Chapter20
open MonskyColor
variable (D : SquareDissection)

Formal statement

lemma ProofsInTheBook.Chapter20.mem_segment_unit_left (p : ℝ × ℝ) :
    p ∈ segment ℝ ((0, 1) : ℝ × ℝ) (0, 0) ↔
      p.1 = 0 ∧ 0 ≤ p.2 ∧ p.2 ≤ 1 := by sorry

Source

Original declaration: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter20E2Boundary.lean#L1134. Repository topic: Monsky’s theorem, “One square and an odd number of triangles.”

View graph