induction_on — Mathlib

English

The same induction principle specialized to AddCommGroup.DirectLimit: a property on the direct limit follows from its validity on all injections of the components.

Русский

Та же индукция для AddCommGroup.DirectLimit: свойство на прямом пределе следует из справедливости на всех впрысках компонентов.

LaTeX

$$$\forall z:\mathrm{DirectLimit}(G,f),\; C(z) \iff \forall i,x, C(\text{of}(G,f,i,x))$$$

Lean4

@[elab_as_elim]
protected theorem induction_on [Nonempty ι] [IsDirected ι (· ≤ ·)] {C : DirectLimit G f → Prop} (z : DirectLimit G f)
    (ih : ∀ i x, C (of G f i x)) : C z :=
  Module.DirectLimit.induction_on z ih

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