ind — Mathlib

English

Induction principle on connected components: If β holds for connectedComponentMk v for all v, then β holds for any c ∈ G.ConnectedComponent.

Русский

Индукционное доказательство по соединённым компонентам: если свойство β выполняется на connectedComponentMk v для всех вершин, то верно и для любого c ∈ G.ConnectedComponent.

LaTeX

$$$\forall \beta : G.ConnectedComponent \to \mathrm{Prop},\ (\forall v : V, \beta(G.connectedComponentMk v)) \to \forall c : G.ConnectedComponent, \beta c$$$

Lean4

@[elab_as_elim]
protected theorem ind {β : G.ConnectedComponent → Prop} (h : ∀ v : V, β (G.connectedComponentMk v))
    (c : G.ConnectedComponent) : β c :=
  Quot.ind h c

Похожие утверждения