V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
c d : V
x✝ : c ∈ C
dnK : ¬d ∈ K
cd : Adj G c d
cnK : ¬c ∈ K
h : componentComplMk G cnK = C
⊢ Reachable (induce (Kᶜ) G) { val := d, property := dnK } { val := c, property := cnK }
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
c d : V
x✝ : c ∈ C
dnK : ¬d ∈ K
cd : Adj G c d
cnK : ¬c ∈ K
h : componentComplMk G cnK = C
⊢ componentComplMk G dnK = C
rw [← h, ConnectedComponent.eq]
no goals
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
c d : V
x✝ : c ∈ C
dnK : ¬d ∈ K
cd : Adj G c d
cnK : ¬c ∈ K
h : componentComplMk G cnK = C
⊢ Reachable (induce (Kᶜ) G) { val := d, property := dnK } { val := c, property := cnK }
exact Adj.reachable cd.symm