ind — Mathlib

English

DivisibleHull carries an induction principle: to prove a property for all elements, it is enough to prove it for mk num den for all nums and dens.

Русский

DivisibleHull поддерживает принцип индукции: чтобы доказать свойство для всех элементов, достаточно доказать его для mk num den для всех числителей и знаменателей.

LaTeX

$$$\text{ind} : \text{(∀ num den, motive (.mk num den))} → ∀ x, motive x$$$

Lean4

@[elab_as_elim, induction_eliminator]
theorem ind {motive : DivisibleHull M → Prop} (mk : ∀ num den, motive (.mk num den)) : ∀ x, motive x :=
  LocalizedModule.induction_on fun m s ↦ mk m (↑ⁿ.symm s)

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