Coordinate description of the unit square’s top segment

Proved

ProofsInTheBook.Chapter20.mem_segment_unit_top

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[(1,1),(0,1)]\quad\Longleftrightarrow\quad 0\leq x\leq1\ \text{and}\ y=1.

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_top (p : ℝ × ℝ) :
    p ∈ segment ℝ ((1, 1) : ℝ × ℝ) (0, 1) ↔
      0 ≤ p.1 ∧ p.1 ≤ 1 ∧ p.2 = 1 := by sorry

Source

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

View graph