Dev/MonadicDependence/NowhereDense/Contract.lean
| 1 | import Mathlib.Combinatorics.SimpleGraph.Copy |
| 2 | import Catalog.Sparsity.Preliminaries.Contract |
| 3 | import Dev.MonadicDependence.Subdivision.Contract |
| 4 | |
| 5 | namespace Dev.MonadicDependence.NowhereDense |
| 6 | |
| 7 | open Catalog.Sparsity.Preliminaries |
| 8 | open Dev.MonadicDependence.Subdivision |
| 9 | |
| 10 | /-- A graph class `𝓒` is *nowhere dense* (Mählmann Def. 13.1, p. 166) |
| 11 | iff for every radius `r : ℕ` there is a bound `N_r : ℕ` such that no |
| 12 | graph in `𝓒` contains the `r`-subdivided clique of order `N_r` |
| 13 | (`subdividedClique N_r r` from `Dev.MonadicDependence.Subdivision`) as |
| 14 | a subgraph. |
| 15 | |
| 16 | This is the *local* nowhere-denseness of Mählmann, distinct from |
| 17 | `Catalog.Sparsity.NowhereDense.IsNowhereDense` (shallow-topological-minor |
| 18 | grad bound). The two are classically equivalent; see |
| 19 | `Dev.MonadicDependence.NowhereDenseBridge`. -/ |
| 20 | def IsNowhereDense (C : GraphClass) : Prop := |
| 21 | ∀ r : ℕ, ∃ N : ℕ, ∀ {V : Type} [DecidableEq V] [Fintype V] (G : SimpleGraph V), |
| 22 | C G → ¬ (subdividedClique N r).IsContained G |
| 23 | |
| 24 | end Dev.MonadicDependence.NowhereDense |
| 25 |