numeric_closed — Mathlib

English

If a' is related to a by ArgsRel and a is numeric, then a' is numeric.

Русский

Если a' относится к a через ArgsRel и a числовой, то a' также числовой.

LaTeX

$$$$ \mathrm{ArgsRel}(a',a) \wedge a.\mathrm{Numeric} \rightarrow a'.\mathrm{Numeric}. $$$$

Lean4

/-- The property that all arguments are numeric is leftward-closed under `ArgsRel`. -/
theorem numeric_closed {a' a} : ArgsRel a' a → a.Numeric → a'.Numeric :=
  TransGen.closed' <| @cutExpand_closed _ IsOption ⟨wf_isOption.isIrrefl.1⟩ _ Numeric.isOption

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