hasSubst_iff_hasEval_of_discreteTopology

English

For discrete topology on S, HasSubst a is equivalent to HasEval a.

Русский

Для дискретной топологии на S HasSubst a эквивалентно HasEval a.

LaTeX

$$$\mathrm{HasSubst}(a) \iff \mathrm{PowerSeries.HasEval}(a)$$$

Lean4

theorem hasSubst_iff_hasEval_of_discreteTopology [TopologicalSpace S] [DiscreteTopology S] {a : MvPowerSeries τ S} :
    HasSubst a ↔ PowerSeries.HasEval a := by
  rw [hasSubst_iff, MvPowerSeries.hasSubst_iff_hasEval_of_discreteTopology, hasEval_iff, Function.const_def]

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