instUniformContinuousConstSMul — Mathlib

English

Convergence of a net a: ι → UniformConvergenceCLM σ F 𝔖 to a0 in the strong topology is equivalent to uniform convergence on every s ∈ 𝔖.

Русский

Сходимость сетки a: ι → UniformConvergenceCLM σ F 𝔖 к a0 в сильной топологии эквивалентна равномерной сходимости на каждом s ∈ 𝔖.

LaTeX

$$$$ \text{Tendsto}(a,p,\mathcal{N}(a_0)) \iff \forall s \in \mathfrak{S}, \ TendstoUniformlyOn(a, a_0, p, s). $$$$

Lean4

instance instUniformContinuousConstSMul (M : Type*) [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜₂ M F]
    [UniformSpace F] [IsUniformAddGroup F] [UniformContinuousConstSMul M F] (𝔖 : Set (Set E)) :
    UniformContinuousConstSMul M (UniformConvergenceCLM σ F 𝔖) :=
  (isUniformInducing_coeFn σ F 𝔖).uniformContinuousConstSMul fun _ _ ↦ by rfl

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