mul_induction_on' — Mathlib

English

Dependent version of the induction principle on M * N: if for all r ∈ M * N, C(r, hr) holds under base cases, then C holds for all r.

Русский

Зависимая версия индукционного принципа на M * N: если для каждого r ∈ M * N верно C(r, hr) при базовых условиях, то C верно для всех r.

LaTeX

$$$ \forall {r : A} (hr : r \in M * N), C r hr \; \Rightarrow \; C r hr$$$

Lean4

/-- A dependent version of `mul_induction_on`. -/
@[elab_as_elim]
protected theorem mul_induction_on' {C : ∀ r, r ∈ M * N → Prop}
    (mem_mul_mem : ∀ m (hm : m ∈ M) n (hn : n ∈ N), C (m * n) (mul_mem_mul hm hn))
    (add : ∀ x hx y hy, C x hx → C y hy → C (x + y) (add_mem hx hy)) {r : A} (hr : r ∈ M * N) : C r hr :=
  smul_induction_on' hr mem_mul_mem add

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