Endpoints of a consecutive unordered edge belong to the list

Proved

ProofsInTheBook.Chapter20.endpoints_mem_of_mem_consecutiveEdges_local

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

auxiliary-lemmageometrylean4monsky-theoremproofs-from-the-book

For any type A, any list l of elements of A, and any $a,b\in A$ , if the unordered pair $\{a,b\}$ occurs in the list of consecutive edges of l, then a and b both occur in l. No decidable-equality, distinctness, no-repetition, geometry, or dissection assumption is required. The unordered pair may have equal entries.

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.endpoints_mem_of_mem_consecutiveEdges_local {α : Type*} {l : List α} {a b : α}
    (h : s(a, b) ∈ consecutiveEdges l) : a ∈ l ∧ b ∈ l := by sorry

Source

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

View graph