Mathlib Map

Theorems Β· Definition Β· functional analysis

ContinuousLinearMap.precompUniformConvergenceCLM

{π•œβ‚ : 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 𝔖

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
2 results in Mathlib
Foundations
Depth 90 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.

ContinuousLinearMap.precomp Β· cited by 13ContinuousLinearMap.preco…PointwiseConvergenceCLM.precomp Β· cited by 2PointwiseConvergenceCLM.p…ContinuousLinearMap.precompCompactConvergenceCLM Β· cited by 2ContinuousLinearMap.preco…ContinuousLinearMap.precompUniformConvergenceCLM_apply Β· cited by 1ContinuousLinearMap.preco…ContinuousLinearMap.precomp_uniformConvergenceCLM Β· cited by 0ContinuousLinearMap.preco…ContinuousLinearMap.precomp_uniformConvergenceCLM_apply Β· cited by 0ContinuousLinearMap.preco…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.MapsToContinuousLinearMap.comp Β· cited by 709ContinuousLinearMap.compRingHomCompTriple Β· cited by 234RingHomCompTripleContinuousLinearMap.precompUn…CITED BYCITES

Cites16

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

Cited by6

Results whose statement or proof uses this declaration.