Mathlib Map

Theorems Β· Definition Β· functional analysis

ContinuousLinearMap.postcomp_uniformConvergenceCLM

Deprecated since 2026-01-27Use ContinuousLinearMap.postcompUniformConvergenceCLM 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)) β†’
                                              [inst_13 : IsTopologicalAddGroup F] β†’
                                                [inst_14 : IsTopologicalAddGroup G] β†’
                                                  [inst_15 : ContinuousConstSMul π•œβ‚ƒ G] β†’
                                                    [inst_16 : ContinuousConstSMul π•œβ‚‚ F] β†’
                                                      (F β†’SL[Ο„] G) β†’
                                                        UniformConvergenceCLM Οƒ F 𝔖 β†’SL[Ο„] UniformConvergenceCLM ρ G 𝔖

Alias of ContinuousLinearMap.postcompUniformConvergenceCLM. Post-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
NormedFieldNormedFieldNormedFieldRingHomCompTripleAddCommGroupModuleAddCommGroupModuleAddCommGroupModuleTopologicalSpaceTopologicalSpaceTopologicalSpaceIsTopologicalAddGroupIsTopologicalAddGroupContinuousConstSMulContinuousConstSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set Β· cited by 53352SetTopologicalSpace Β· cited by 24529TopologicalSpaceModule Β· cited by 20661ModuleAddCommGroup Β· cited by 12871AddCommGroupRingHom Β· cited by 10189RingHomContinuousLinearMap Β· cited by 5352ContinuousLinearMapIsTopologicalAddGroup Β· cited by 1394IsTopologicalAddGroupNormedField Β· cited by 1084NormedFieldContinuousConstSMul Β· cited by 832ContinuousConstSMulRingHomCompTriple Β· cited by 234RingHomCompTripleUniformConvergenceCLM Β· cited by 44UniformConvergenceCLMContinuousLinearMap.postcompUniformConvergenceCLM Β· cited by 2ContinuousLinearMap.postc…ContinuousLinearMap.postcomp_…CITED BYCITES

Cites12

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.