Proof of `Trees are outerplanar`

conditional — 1 open assumptionproofs/Lax68Proofs/ForestMinors.lean · lax-68

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

A tree is acyclic, and so are all its minors. The triangle in K4K₄ and the four-cycle in K2,3K₂,₃ therefore exclude both as minors. Apply the excluded-minor characterization of outerplanarity, which remains open in this submission.