Catalog.Sparsity.UQWEquivND
Theorem
A class \(\mathcal{C}\) of graphs is uniformly quasi-wide (Definition UniformQuasiWideness) if and only if it is nowhere dense (Definition NowhereDense).
Review notes
The Lean statement is an iff, directly matching Theorem 3.2 of the source. The proof (Phase 4) combines the two directions:
- Forward (UQW \(\Rightarrow\) ND):
Catalog.Sparsity.UQWImpliesND.uqw_implies_nd - Backward (ND \(\Rightarrow\) UQW):
Catalog.Sparsity.NDImpliesUQW.nd_implies_uqw
Catalog/Sparsity/UQWEquivND/Contract.lean (full)
| 1 | import Catalog.Sparsity.Preliminaries.Contract |
| 2 | import Catalog.Sparsity.NowhereDense.Contract |
| 3 | import Catalog.Sparsity.UniformQuasiWideness.Contract |
| 4 | |
| 5 | namespace Catalog.Sparsity.UQWEquivND |
| 6 | |
| 7 | open Catalog.Sparsity.Preliminaries Catalog.Sparsity.NowhereDense Catalog.Sparsity.UniformQuasiWideness |
| 8 | |
| 9 | /-- Theorem 3.2: a class of graphs is uniformly quasi-wide if and only if it is |
| 10 | nowhere dense. -/ |
| 11 | axiom uqw_iff_nd (C : GraphClass) : |
| 12 | UniformlyQuasiWide C ↔ IsNowhereDense C |
| 13 | |
| 14 | end Catalog.Sparsity.UQWEquivND |
| 15 |