Mathlib Map

Theorems ยท Definition ยท functional analysis

ContinuousLinearMap.precomp_uniformConvergenceCLM

Deprecated since 2026-01-27Use ContinuousLinearMap.precompUniformConvergenceCLM instead.

{๐•œโ‚ : Type u_6} โ†’
  {๐•œโ‚‚ : Type u_7} โ†’
    {๐•œโ‚ƒ : Type u_8} โ†’
      [inst : NormedField ๐•œโ‚] โ†’
        [inst_1 : NormedField ๐•œโ‚‚] โ†’
          [inst_2 : NormedField ๐•œโ‚ƒ] โ†’
            {ฯƒ : ๐•œโ‚ โ†’+* ๐•œโ‚‚} โ†’
              {ฯ„ : ๐•œโ‚‚ โ†’+* ๐•œโ‚ƒ} โ†’
                {ฯ : ๐•œโ‚ โ†’+* ๐•œโ‚ƒ} โ†’
                  [RingHomCompTriple ฯƒ ฯ„ ฯ] โ†’
                    {E : Type u_9} โ†’
                      {F : Type u_10} โ†’
                        (G : Type u_11) โ†’
                          [inst_4 : AddCommGroup E] โ†’
                            [inst_5 : Module ๐•œโ‚ E] โ†’
                              [inst_6 : AddCommGroup F] โ†’
                                [inst_7 : Module ๐•œโ‚‚ F] โ†’
                                  [inst_8 : AddCommGroup G] โ†’
                                    [inst_9 : Module ๐•œโ‚ƒ G] โ†’
                                      [inst_10 : TopologicalSpace E] โ†’
                                        [inst_11 : TopologicalSpace F] โ†’
                                          [inst_12 : TopologicalSpace G] โ†’
                                            (๐”– : Set (Set E)) โ†’
                                              (๐”— : Set (Set F)) โ†’
                                                [inst_13 : IsTopologicalAddGroup G] โ†’
                                                  [inst_14 : ContinuousConstSMul ๐•œโ‚ƒ G] โ†’
                                                    (L : E โ†’SL[ฯƒ] F) โ†’
                                                      Set.MapsTo (fun x => โ‡‘L '' x) ๐”– ๐”— โ†’
                                                        UniformConvergenceCLM ฯ„ G ๐”— โ†’L[๐•œโ‚ƒ] UniformConvergenceCLM ฯ G ๐”–

Alias of ContinuousLinearMap.precompUniformConvergenceCLM. Pre-composition by a fixed continuous linear map as a continuous linear map for the uniform convergence topology.

Defined in
Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
Cited by
0 results in Mathlib
Foundations
Depth 91 from the axioms ยท uses propext, Classical.choice, Quot.sound
Assumes
NormedFieldNormedFieldNormedFieldRingHomCompTripleAddCommGroupModuleAddCommGroupModuleAddCommGroupModuleTopologicalSpaceTopologicalSpaceTopologicalSpaceIsTopologicalAddGroupContinuousConstSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

DFunLike.coe ยท cited by 62936DFunLike.coeSet ยท cited by 53352SetTopologicalSpace ยท cited by 24529TopologicalSpaceModule ยท cited by 20661ModuleRingHom.id ยท cited by 18349RingHom.idAddCommGroup ยท cited by 12871AddCommGroupRingHom ยท cited by 10189RingHomSet.image ยท cited by 5609Set.imageContinuousLinearMap ยท cited by 5352ContinuousLinearMapIsTopologicalAddGroup ยท cited by 1394IsTopologicalAddGroupNormedField ยท cited by 1084NormedFieldContinuousConstSMul ยท cited by 832ContinuousConstSMulSet.MapsTo ยท cited by 732Set.MapsToRingHomCompTriple ยท cited by 234RingHomCompTripleUniformConvergenceCLM ยท cited by 44UniformConvergenceCLMContinuousLinearMap.precomp_uโ€ฆCITED BYCITES

Cites16

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.