Mathlib Map

Theorems Β· Definition Β· functional analysis

PointwiseConvergenceCLM.postcomp

{π•œβ‚ : Type u_4} β†’
  {π•œβ‚‚ : Type u_5} β†’
    {π•œβ‚ƒ : Type u_6} β†’
      [inst : NormedField π•œβ‚] β†’
        [inst_1 : NormedField π•œβ‚‚] β†’
          [inst_2 : NormedField π•œβ‚ƒ] β†’
            {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} β†’
              {Ο„ : π•œβ‚‚ β†’+* π•œβ‚ƒ} β†’
                {ρ : π•œβ‚ β†’+* π•œβ‚ƒ} β†’
                  [RingHomCompTriple Οƒ Ο„ ρ] β†’
                    (E : Type u_7) β†’
                      {F : Type u_8} β†’
                        {G : Type u_10} β†’
                          [inst_4 : AddCommGroup E] β†’
                            [inst_5 : TopologicalSpace E] β†’
                              [inst_6 : AddCommGroup F] β†’
                                [inst_7 : TopologicalSpace F] β†’
                                  [inst_8 : IsTopologicalAddGroup F] β†’
                                    [inst_9 : AddCommGroup G] β†’
                                      [inst_10 : TopologicalSpace G] β†’
                                        [inst_11 : IsTopologicalAddGroup G] β†’
                                          [inst_12 : Module π•œβ‚ E] β†’
                                            [inst_13 : Module π•œβ‚‚ F] β†’
                                              [inst_14 : Module π•œβ‚ƒ G] β†’
                                                [inst_15 : ContinuousConstSMul π•œβ‚‚ F] β†’
                                                  [inst_16 : ContinuousConstSMul π•œβ‚ƒ G] β†’
                                                    (F β†’SL[Ο„] G) β†’ (E β†’SLβ‚šβ‚œ[Οƒ] F) β†’SL[Ο„] E β†’SLβ‚šβ‚œ[ρ] G

Post-composition by a fixed continuous linear map as a continuous linear map for the pointwise convergence topology.

Defined in
Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
Cited by
1 results in Mathlib
Foundations
Depth 92 from the axioms Β· uses propext, Classical.choice, Quot.sound
Assumes
NormedFieldNormedFieldNormedFieldRingHomCompTripleAddCommGroupTopologicalSpaceAddCommGroupTopologicalSpaceIsTopologicalAddGroupAddCommGroupTopologicalSpaceIsTopologicalAddGroupModuleModuleModuleContinuousConstSMulContinuousConstSMul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

PointwiseConvergenceCLM.postcomp_apply Β· cited by 0PointwiseConvergenceCLM.p…Set Β· cited by 53352SetTopologicalSpace Β· cited by 24529TopologicalSpaceModule Β· cited by 20661ModuleAddCommGroup Β· cited by 12871AddCommGroupRingHom Β· cited by 10189RingHomSet.Elem Β· cited by 7166Set.ElemSet.ofPred Β· cited by 6101Set.ofPredContinuousLinearMap Β· cited by 5352ContinuousLinearMapFinite Β· cited by 3029FiniteIsTopologicalAddGroup Β· cited by 1394IsTopologicalAddGroupNormedField Β· cited by 1084NormedFieldContinuousConstSMul Β· cited by 832ContinuousConstSMulContinuousLinearMap.comp Β· cited by 709ContinuousLinearMap.compRingHomCompTriple Β· cited by 234RingHomCompTripleUniformConvergenceCLM Β· cited by 44UniformConvergenceCLMPointwiseConvergenceCLM.postc…CITED BYCITES

Cites17

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

Cited by1

Results whose statement or proof uses this declaration.