induction_on' — Mathlib

English

Let P be a property of RatFunc K. If P holds for every representative mk p q (i.e., for all p, q with q ≠ 0, P(mk p q)), then P holds for every element of RatFunc K.

Русский

Пусть P — свойство RatFunc K. Если P выполняется для каждого представителя mk p q (то есть для всех p, q при q ≠ 0, P(mk p q)), тогда P выполняется для любого элемента RatFunc K.

LaTeX

$$$\\forall P:\\\\mathrm{RatFunc}K \\to \\mathrm{Prop},\\;\\big(\\\\forall p,q:\\\\mathbb{K}[X],\\\\; q \\neq 0 \\Rightarrow P(\\\\mathrm{RatFunc.mk}\\,p\\,q)\\big) \\Rightarrow \\forall x\\, P(x)$$$

Lean4

/-- Induction principle for `RatFunc K`: if `f p q : P (RatFunc.mk p q)` for all `p q`,
then `P` holds on all elements of `RatFunc K`.

See also `induction_on`, which is a recursion principle defined in terms of `algebraMap`.
-/
@[elab_as_elim]
protected theorem induction_on' {P : RatFunc K → Prop} :
    ∀ (x : RatFunc K) (_pq : ∀ (p q : K[X]) (_ : q ≠ 0), P (RatFunc.mk p q)), P x
  | ⟨x⟩, f =>
    Localization.induction_on x fun ⟨p, q⟩ => by
      simpa only [mk_coe_def, Localization.mk_eq_mk'] using f p q (mem_nonZeroDivisors_iff_ne_zero.mp q.2)

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