Lax5.AdlerAdler
Nowhere dense classes are monadically dependent
concepts/Lax5/AdlerAdler.lean · Lax5
Theorem
Every nowhere dense graph class is monadically dependent. Together with the statement that weakly sparse monadically dependent classes are nowhere dense, this carries the classical equivalence: on weakly sparse classes, monadic dependence and nowhere denseness coincide.
Lean source view on GitHub
| 1 | import Lax5.MonadicDependence |
| 2 | import Lax5.NowhereDenseClasses |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Nowhere dense classes are monadically dependent |
| 7 | type: theorem |
| 8 | --- |
| 9 | Every nowhere dense graph class is monadically dependent. Together with |
| 10 | the statement that weakly sparse monadically dependent classes are |
| 11 | nowhere dense, this carries the classical equivalence: on weakly sparse |
| 12 | classes, monadic dependence and nowhere denseness coincide. |
| 13 | |
| 14 | # Formalization notes |
| 15 | |
| 16 | Adler and Adler proved that nowhere dense classes are monadically |
| 17 | *stable*; monadic dependence is the weakening stated here, which is how |
| 18 | the equivalence is used in the literature. |
| 19 | -/ |
| 20 | |
| 21 | namespace Lax5.AdlerAdler |
| 22 | |
| 23 | open Lax5.GraphClasses Lax5.MonadicDependence Lax5.NowhereDenseClasses |
| 24 | |
| 25 | /-- Nowhere dense graph classes are monadically dependent. -/ |
| 26 | axiom monadicallyDependent_of_nowhereDense |
| 27 | (C : GraphClass) (h : NowhereDense C) : |
| 28 | MonadicallyDependent C |
| 29 | |
| 30 | end Lax5.AdlerAdler |
| 31 |
Formalization notes
Adler and Adler proved that nowhere dense classes are monadically stable; monadic dependence is the weakening stated here, which is how the equivalence is used in the literature.
Imported by
none
Mathlib imports
none