case h
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : ComponentCompl G K → Prop
f : ∀ ⦃v : V⦄ (hv : ¬v ∈ K), β (componentComplMk G hv)
⊢ ∀ (v : ↑(Kᶜ)), β (connectedComponentMk (induce (Kᶜ) G) v)
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : ComponentCompl G K → Prop
f : ∀ ⦃v : V⦄ (hv : ¬v ∈ K), β (componentComplMk G hv)
⊢ ∀ (C : ComponentCompl G K), β C
apply ConnectedComponent.ind
no goals
case h
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : ComponentCompl G K → Prop
f : ∀ ⦃v : V⦄ (hv : ¬v ∈ K), β (componentComplMk G hv)
⊢ ∀ (v : ↑(Kᶜ)), β (connectedComponentMk (induce (Kᶜ) G) v)
exact fun ⟨v, vnK⟩ => f vnK