induction_on₂ — Mathlib

English

If a property holds for mk m s and mk m' s', then it holds for all pairs x y in LocalizedModule S M.

Русский

Если свойство верно для mk m s и mk m' s', то оно верно для любых пары x,y в LocalizedModule S M.

LaTeX

$$$\\forall x,y,\\, P(x,y) \\Leftarrow P(\\mk m s, \\mk m' s').$$$

Lean4

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

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