uniformContinuous_eval₂ — Mathlib

English

The evaluation map is uniformly continuous with respect to the base uniform structures, under the given hypotheses.

Русский

Оценивание является равномерно непрерывным относительно базовых структур равномерности при заданных гипотезах.

LaTeX

$$$$\operatorname{UniformContinuous}(\operatorname{eval}_{\phi}^{a}).$$$$

Lean4

theorem uniformContinuous_eval₂ (hφ : Continuous φ) (ha : HasEval a) : UniformContinuous (eval₂ φ a) :=
  by
  rw [← coe_eval₂Hom hφ ha]
  exact
    uniformContinuous_uniformly_extend toMvPowerSeries_isUniformInducing denseRange_toMvPowerSeries
      (toMvPowerSeries_uniformContinuous hφ ha)

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