Prove2Me

The frontier of the closed unit square

Proved
ProofsInTheBook.Chapter20.Chapter20E2Frontier.frontier_unitSquare

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

auxiliary-lemmageometrylean4monsky-theoremproofs-from-the-book

In the real plane,

∂([0,1]2)={(x,y):0≤x≤1, 0≤y≤1, x=0 or x=1 or y=0 or y=1}.\partial([0,1]^2)=\{(x,y):0\leq x\leq1,\ 0\leq y\leq1,\ x=0\ \text{or}\ x=1\ \text{or}\ y=0\ \text{or}\ y=1\}.

The frontier is taken in the ordinary topology of the plane. There are no dissection or coloring hypotheses.

Preamble
import Init
import Mathlib
import Definitions.Def_P2MAssembly_Chapter20
set_option autoImplicit true
open ProofsInTheBook.Chapter20
open scoped Topology
open ProofsInTheBook.Chapter20.Chapter20E2Frontier
Formal statement
theorem ProofsInTheBook.Chapter20.Chapter20E2Frontier.frontier_unitSquare :
    frontier (Set.Icc ((0, 0) : P) (1, 1)) =
      {p : P | 0 ≤ p.1 ∧ p.1 ≤ 1 ∧ 0 ≤ p.2 ∧ p.2 ≤ 1 ∧
        (p.1 = 0 ∨ p.1 = 1 ∨ p.2 = 0 ∨ p.2 = 1)} := by sorry
Source
Original declaration: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter20E2Frontier.lean#L586. Repository topic: Monsky’s theorem, “One square and an odd number of triangles.”

View graph