hasEval_iff — Mathlib

English

HasEval a holds if and only if the multivariate power-series HasEval of the constant map to a holds; equivalently.

Русский

HasEval a верно тогда и только тогда, когда HasEval для многомерного ряда от a также верно; эквивалентно.

LaTeX

$$$ HasEval(a) \\Leftrightarrow MvPowerSeries.HasEval (fun _ : Unit \\mapsto a) $$$

Lean4

theorem hasEval_iff {a : S} : HasEval a ↔ MvPowerSeries.HasEval (fun (_ : Unit) ↦ a) :=
  ⟨fun ha ↦ ⟨fun _ ↦ ha, by simp⟩, fun ha ↦ ha.hpow default⟩

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