Theorems · Definition · functional analysis

continuousLinearMapOfTendsto

{α : Type u_1} →
  {𝕜₁ : Type u_4} →
    {𝕜₂ : Type u_5} →
      {E : Type u_6} →
        {F : Type u_7} →
          [inst : NontriviallyNormedField 𝕜₁] →
            [inst_1 : NontriviallyNormedField 𝕜₂] →
              {σ₁₂ : 𝕜₁ →+* 𝕜₂} →
                [RingHomIsometric σ₁₂] →
                  [inst_3 : AddCommGroup E] →
                    [inst_4 : AddCommGroup F] →
                      [inst_5 : Module 𝕜₁ E] →
                        [inst_6 : Module 𝕜₂ F] →
                          [inst_7 : UniformSpace E] →
                            [inst_8 : UniformSpace F] →
                              [IsUniformAddGroup E] →
                                [IsUniformAddGroup F] →
                                  [ContinuousSMul 𝕜₁ E] →
                                    [BarrelledSpace 𝕜₁ E] →
                                      [PolynormableSpace 𝕜₂ F] →
                                        [ContinuousSMul 𝕜₂ F] →
                                          [T2Space F] →
                                            {l : Filter α} →
                                              [l.IsCountablyGenerated] →
                                                [l.NeBot] →
                                                  (g : α → E →SL[σ₁₂] F) →
                                                    {f : E → F} →
                                                      Filter.Tendsto (fun n x => (g n) x) l (nhds f) → E →SL[σ₁₂] F

Given a sequence of continuous linear maps which converges pointwise and for which the domain is barrelled, the Banach-Steinhaus theorem is used to guarantee that the limit map is a continuous linear map as well. This actually works for any countably generated filter instead of atTop : Filter ℕ, but the proof ultimately goes back to sequences.

Defined in

Mathlib.Analysis.LocallyConvex.Barrelled

Cited by

0 results in Mathlib

Foundations

Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNontriviallyNormedFieldRingHomIsometricAddCommGroupAddCommGroupModuleModuleUniformSpaceUniformSpaceIsUniformAddGroupIsUniformAddGroupContinuousSMulBarrelledSpacePolynormableSpaceContinuousSMulT2SpaceFilter.IsCountablyGeneratedFilter.NeBot