Lax Lean Archive

Proof of `Walls are planar`

groundedproofs/Lax68Proofs/Relationships.lean · lax-68

What this proof establishes

thm✓Lax68.WallPlanar

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

A wall uses a subset of the edges of its rectangular grid. Restrict a planar grid drawing to those edges and relabel its vertices by the wall isomorphism.