numeric_option_mul — Mathlib

English

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

Русский

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

LaTeX

$$$\forall x\forall x'\forall y\big(\big(\forall a\; ArgsRel(a, Args.P1\ x\ y) \rightarrow P124\ a\big) \rightarrow IsOption(x',x) \rightarrow (x' * y).Numeric\big)$$$

Lean4

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

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