Lax5.WeaklySparseDependent
Weakly sparse monadically dependent classes are nowhere dense
concepts/Lax5/WeaklySparseDependent.lean · Lax5
Theorem
A graph class is weakly sparse if some complete bipartite graph K_{t,t} occurs in no member as a subgraph. Every weakly sparse monadically dependent graph class is nowhere dense.
Lean source view on GitHub
| 1 | import Lax5.MonadicDependence |
| 2 | import Lax5.NowhereDenseClasses |
| 3 | import Mathlib.Combinatorics.SimpleGraph.Copy |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Weakly sparse monadically dependent classes are nowhere dense |
| 8 | type: theorem |
| 9 | --- |
| 10 | A graph class is weakly sparse if some complete bipartite graph |
| 11 | K_{t,t} occurs in no member as a subgraph. Every weakly sparse |
| 12 | monadically dependent graph class is nowhere dense. |
| 13 | |
| 14 | # Formalization notes |
| 15 | |
| 16 | Subgraph containment is mathlib's `⊑` (an injective homomorphism of |
| 17 | `completeBipartiteGraph (Fin t) (Fin t)` into the member). The value |
| 18 | `t = 0` does not trivialize weak sparseness: the empty graph is |
| 19 | contained in every graph, so `¬ K_{0,0} ⊑ G` never holds and no side |
| 20 | condition on `t` is needed. `WeaklySparse` is defined here rather than |
| 21 | in the graph classes concept because this statement is its only use. |
| 22 | -/ |
| 23 | |
| 24 | namespace Lax5.WeaklySparseDependent |
| 25 | |
| 26 | open scoped SimpleGraph |
| 27 | open Lax5.GraphClasses Lax5.MonadicDependence Lax5.NowhereDenseClasses |
| 28 | |
| 29 | /-- A graph class is weakly sparse if some complete bipartite graph |
| 30 | `K_{t,t}` occurs in no member as a subgraph. -/ |
| 31 | def WeaklySparse (C : GraphClass) : Prop := |
| 32 | ∃ t : ℕ, ∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G → |
| 33 | ¬ completeBipartiteGraph (Fin t) (Fin t) ⊑ G |
| 34 | |
| 35 | /-- Every weakly sparse monadically dependent graph class is nowhere |
| 36 | dense. -/ |
| 37 | axiom nowhereDense_of_weaklySparse_of_monadicallyDependent |
| 38 | (C : GraphClass) (hs : WeaklySparse C) (hd : MonadicallyDependent C) : |
| 39 | NowhereDense C |
| 40 | |
| 41 | end Lax5.WeaklySparseDependent |
| 42 |
Formalization notes
Subgraph containment is mathlib's ⊑ (an injective homomorphism of
completeBipartiteGraph (Fin t) (Fin t) into the member). The value
t = 0 does not trivialize weak sparseness: the empty graph is
contained in every graph, so ¬ K_{0,0} ⊑ G never holds and no side
condition on t is needed. WeaklySparse is defined here rather than
in the graph classes concept because this statement is its only use.
Imported by
none