ind₂ — Mathlib

English

Double induction principle on connected components: if β holds for the pair of components corresponding to any vertices, then β holds for any pair of components.

Русский

Двойной принцип индукции по двум соединённым компонентам: если β верно для пары компонент, соответствующих любым вершинам, то верно и для любой пары компонент.

LaTeX

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

Lean4

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

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