continuousEvalConst — Mathlib

English

Alternative version asserting T2 property for UniformConvergenceCLM under similar hypotheses.

Русский

Альтернативная версия утверждает свойство T2 для UniformConvergenceCLM при аналогичных предпосылках.

LaTeX

$$$\\text{t2Space}(\\sigma,F,\\mathcal{S})$$$

Lean4

theorem continuousEvalConst [TopologicalSpace F] [IsTopologicalAddGroup F] (𝔖 : Set (Set E)) (h𝔖 : ⋃₀ 𝔖 = Set.univ) :
    ContinuousEvalConst (UniformConvergenceCLM σ F 𝔖) E F where
  continuous_eval_const
    x := by
    letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
    haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
    exact (UniformOnFun.uniformContinuous_eval h𝔖 x).continuous.comp (isEmbedding_coeFn σ F 𝔖).continuous

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