induction_on — Mathlib

English

To prove a property for all AEEqFun, it suffices to prove it for all mk f hf.

Русский

Чтобы доказать свойство для всех AEeqFun, достаточно доказать его для всех mk f hf.

LaTeX

$$$\\forall f\\,\\forall hf:\\; p(\\mathrm{mk} f hf)\\Rightarrow p(f)$$$

Lean4

@[elab_as_elim]
theorem induction_on (f : α →ₘ[μ] β) {p : (α →ₘ[μ] β) → Prop} (H : ∀ f hf, p (mk f hf)) : p f :=
  Quotient.inductionOn' f <| Subtype.forall.2 H

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