numeric_mul_option — Mathlib

English

If the induction hypothesis IH holds for x and y, and y′ is an option of y, then x·y′ is numeric.

Русский

Если IH справедливо для x и y, и y′ является опцией y, тогда x·y′ численно.

LaTeX

$$$\forall x\forall y\forall y'\big( IsOption(y',y) \rightarrow (x * y').Numeric \big)$$$

Lean4

theorem numeric_mul_option (ih : ∀ a, ArgsRel a (Args.P1 x y) → P124 a) (h : IsOption y' y) : (x * y').Numeric :=
  ih (Args.P1 x y') (TransGen.single <| cutExpand_pair_right h)

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