Mathlib Map

Theorems Β· Definition Β· functional analysis

ContinuousLinearMap.postcompUniformConvergenceCLM

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

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

ContinuousLinearMap.postcomp Β· cited by 17ContinuousLinearMap.postc…ContinuousLinearMap.postcompCompactConvergenceCLM Β· cited by 2ContinuousLinearMap.postc…PointwiseConvergenceCLM.postcomp Β· cited by 1PointwiseConvergenceCLM.p…ContinuousLinearMap.postcompUniformConvergenceCLM_apply Β· cited by 1ContinuousLinearMap.postc…ContinuousLinearMap.postcomp_uniformConvergenceCLM Β· cited by 0ContinuousLinearMap.postc…ContinuousLinearMap.postcomp_uniformConvergenceCLM_apply Β· cited by 0ContinuousLinearMap.postc…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 832ContinuousConstSMulContinuousLinearMap.comp Β· cited by 709ContinuousLinearMap.compRingHomCompTriple Β· cited by 234RingHomCompTripleUniformConvergenceCLM Β· cited by 44UniformConvergenceCLMContinuousLinearMap.postcompU…CITED BYCITES

Cites12

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.