Catalog/Sparsity/UQWEquivND/Full.lean
| 1 | import Catalog.Sparsity.Preliminaries.Full |
| 2 | import Catalog.Sparsity.NowhereDense.Full |
| 3 | import Catalog.Sparsity.UniformQuasiWideness.Full |
| 4 | import Catalog.Sparsity.UQWImpliesND.Full |
| 5 | import Catalog.Sparsity.NDImpliesUQW.Full |
| 6 | |
| 7 | namespace Catalog.Sparsity.UQWEquivND |
| 8 | |
| 9 | open Catalog.Sparsity.Preliminaries Catalog.Sparsity.NowhereDense Catalog.Sparsity.UniformQuasiWideness |
| 10 | |
| 11 | /-- Theorem 3.2: a class of graphs is uniformly quasi-wide if and only if it is |
| 12 | nowhere dense. -/ |
| 13 | theorem uqw_iff_nd (C : GraphClass) : |
| 14 | UniformlyQuasiWide C ↔ IsNowhereDense C := by |
| 15 | exact ⟨Catalog.Sparsity.UQWImpliesND.uqw_implies_nd C, Catalog.Sparsity.NDImpliesUQW.nd_implies_uqw C⟩ |
| 16 | |
| 17 | end Catalog.Sparsity.UQWEquivND |
| 18 |