inductionOn — Mathlib

English

An induction principle for germs: to prove a property for every germ, it suffices to prove it for all representatives.

Русский

Индукционная принципиальная формулировка для зародышей: чтобы доказать свойство для каждого зародыша, достаточно доказать его для всех представлений.

LaTeX

$$$ \text{inductionOn } (f : \mathrm{Germ}(l, \beta)) \, {p : \mathrm{Germ}(l, \beta) \to \text{Prop}} \, (h : \forall f : \alpha \to \beta, p(\mathrm{Germ.ofFun}(f))) \, \Rightarrow \, p(f)$$$

Lean4

@[elab_as_elim]
theorem inductionOn (f : Germ l β) {p : Germ l β → Prop} (h : ∀ f : α → β, p f) : p f :=
  Quotient.inductionOn' f h

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