V : Type u
G✝ : SimpleGraph V
K L L' M : Set V
G : SimpleGraph V
v w : V
vK : ¬v ∈ K
wK : ¬w ∈ K
a : Adj G v w
⊢ Reachable (induce (Kᶜ) G) { val := v, property := vK } { val := w, property := wK }
V : Type u
G✝ : SimpleGraph V
K L L' M : Set V
G : SimpleGraph V
v w : V
vK : ¬v ∈ K
wK : ¬w ∈ K
a : Adj G v w
⊢ componentComplMk G vK = componentComplMk G wK
rw [ConnectedComponent.eq]
case h
V : Type u
G✝ : SimpleGraph V
K L L' M : Set V
G : SimpleGraph V
v w : V
vK : ¬v ∈ K
wK : ¬w ∈ K
a : Adj G v w
⊢ Adj (induce (Kᶜ) G) { val := v, property := vK } { val := w, property := wK }
V : Type u
G✝ : SimpleGraph V
K L L' M : Set V
G : SimpleGraph V
v w : V
vK : ¬v ∈ K
wK : ¬w ∈ K
a : Adj G v w
⊢ Reachable (induce (Kᶜ) G) { val := v, property := vK } { val := w, property := wK }
apply Adj.reachable
no goals
case h
V : Type u
G✝ : SimpleGraph V
K L L' M : Set V
G : SimpleGraph V
v w : V
vK : ¬v ∈ K
wK : ¬w ∈ K
a : Adj G v w
⊢ Adj (induce (Kᶜ) G) { val := v, property := vK } { val := w, property := wK }
exact a