English
An induction principle for components outside K: to prove a property P holds for every C in G.ComponentCompl K, it suffices to prove P on the canonical component corresponding to each vertex v ∉ K.
Русский
Индукционное принцип для компонент вне K: чтобы доказать свойство P для каждой компонентны G.ComponentCompl K, достаточно доказать P для канонической компоненты, соответствующей каждому вершине v, не принадлежащей K.
LaTeX
$$$$ \forall \beta:\ G.ComponentCompl K \to \text{Prop}, \ \big( \forall \{v\}, v \notin K \to \beta( G.componentComplMk \{v\,\text{вне }K\}) \big) \to \forall C:\ G.ComponentCompl K, \ \beta C $$$$
Lean4
@[elab_as_elim]
protected theorem ind {β : G.ComponentCompl K → Prop} (f : ∀ ⦃v⦄ (hv : v ∉ K), β (G.componentComplMk hv)) :
∀ C : G.ComponentCompl K, β C := by
apply ConnectedComponent.ind
exact fun ⟨v, vnK⟩ => f vnK
