ConnectedLevels.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PlanarRecursion.preconnected_color_constant line 14
theorem OAI.HyperbolicObstruction.PlanarRecursion.connected_avoids_level line 31
Source documentation
A connected set avoiding an integer level cannot pass from below to above it when adjacent depths differ by at most one. Isolated/empty induced graphs are covered by Preconnected, with no global connectedness or positivity assumption.
```
theorem connected_avoids_level (G : SimpleGraph V) (depth : V → ℤ)
    (hd : ∀ v w, G.Adj v w → depth v ≤ depth w+1 ∧ depth w ≤ depth v+1)
    (U : Set V) (hc : (G.induce U).Preconnected) (z : ℤ)
    (hz : ∀ v ∈ U, depth v ≠ z) :
    ∀ v ∈ U, ∀ w ∈ U, (depth v < z ↔ depth w < z) := by
…
```
lemma OAI.HyperbolicObstruction.PlanarRecursion.graph_dist_int_adj line 46