Proof of `Asteroidal cycle triples obstruct induced minors` (2nd statement)

groundedproofs/Lax762056Proofs/GridWitness.lean · lax-762056

What this proof establishes

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

Three corner squares form an asteroidal triple, joined pairwise by paths along the boundary of the grid.