Theorems · Theorem · combinatorics

SimpleGraph.ComponentCompl.mem_of_adj

∀ {V : Type u} {G : SimpleGraph V} {K : Set V} {C : G.ComponentCompl K} (c d : V), c ∈ C → d ∉ K → G.Adj c d → d ∈ C

Any vertex adjacent to a vertex of C and not lying in K must lie in C.

Defined in

Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Cited by

1 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound