induction_on — Mathlib

English

Every localized element can be generated from a representative mk m s by induction on mk.

Русский

Каждый локализованный элемент порождается представителем mk m s, что следует из индукции по mk.

LaTeX

$$$\\text{induction_on} : \\forall x, \\beta(x) \\text{ от } \\beta(\\text{mk}(m,s)).$$$

Lean4

@[elab_as_elim, induction_eliminator, cases_eliminator]
theorem induction_on {β : LocalizedModule S M → Prop} (h : ∀ (m : M) (s : S), β (mk m s)) :
    ∀ x : LocalizedModule S M, β x := by
  rintro ⟨⟨m, s⟩⟩
  exact h m s

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