Mathlib Map

Theorems Β· Definition Β· functional analysis

ContinuousLinearMapWOT.comp

{π•œβ‚ : Type u_5} β†’
  {π•œβ‚‚ : Type u_6} β†’
    {π•œβ‚ƒ : Type u_7} β†’
      {E : Type u_9} β†’
        {F : Type u_10} β†’
          {G : Type u_11} β†’
            [inst : NormedField π•œβ‚] β†’
              [inst_1 : NormedField π•œβ‚‚] β†’
                [inst_2 : NormedField π•œβ‚ƒ] β†’
                  {σ₁₂ : π•œβ‚ β†’+* π•œβ‚‚} β†’
                    {σ₁₃ : π•œβ‚ β†’+* π•œβ‚ƒ} β†’
                      {σ₂₃ : π•œβ‚‚ β†’+* π•œβ‚ƒ} β†’
                        [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] β†’
                          [inst_4 : AddCommGroup E] β†’
                            [inst_5 : TopologicalSpace E] β†’
                              [inst_6 : Module π•œβ‚ E] β†’
                                [inst_7 : AddCommGroup F] β†’
                                  [inst_8 : TopologicalSpace F] β†’
                                    [inst_9 : Module π•œβ‚‚ F] β†’
                                      [inst_10 : AddCommGroup G] β†’
                                        [inst_11 : TopologicalSpace G] β†’
                                          [inst_12 : Module π•œβ‚ƒ G] β†’ (F β†’SWOT[σ₂₃] G) β†’ (E β†’SWOT[σ₁₂] F) β†’ E β†’SWOT[σ₁₃] G

Composition of continuous linear maps on the type synonym equipped with the weak operator topology.

Defined in
Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
Cited by
11 results in Mathlib
Foundations
Depth 45 from the axioms Β· uses propext, Quot.sound
Assumes
NormedFieldNormedFieldNormedFieldRingHomCompTripleAddCommGroupTopologicalSpaceModuleAddCommGroupTopologicalSpaceModuleAddCommGroupTopologicalSpaceModule
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ContinuousLinearMapWOT.postcompCLM Β· cited by 1ContinuousLinearMapWOT.po…ContinuousLinearMapWOT.precompCLM Β· cited by 1ContinuousLinearMapWOT.pr…ContinuousLinearMapWOT.comp_apply Β· cited by 1ContinuousLinearMapWOT.co…ContinuousLinearMapWOT.postcompCLM_apply Β· cited by 0ContinuousLinearMapWOT.po…ContinuousLinearMapWOT.precompCLM_apply Β· cited by 0ContinuousLinearMapWOT.pr…ContinuousLinearMapWOT.comp_assoc Β· cited by 0ContinuousLinearMapWOT.co…ContinuousLinearMapWOT.comp_id Β· cited by 0ContinuousLinearMapWOT.co…ContinuousLinearMapWOT.id_comp Β· cited by 0ContinuousLinearMapWOT.id…ContinuousLinearMapWOT.mul_eq_comp Β· cited by 0ContinuousLinearMapWOT.mu…ContinuousLinearMapWOT.comp.congr_simp Β· cited by 0comp.congr_simpContinuousLinearMapWOT.toCLM_comp Β· cited by 0ContinuousLinearMapWOT.to…ContinuousLinearMapWOT.continuous_postcomp Β· cited by 0ContinuousLinearMapWOT.co…ContinuousLinearMapWOT.continuous_precomp Β· cited by 0ContinuousLinearMapWOT.co…TopologicalSpace Β· cited by 24529TopologicalSpaceModule Β· cited by 20661ModuleAddCommGroup Β· cited by 12871AddCommGroupRingHom Β· cited by 10189RingHomNormedField Β· cited by 1084NormedFieldContinuousLinearMap.comp Β· cited by 709ContinuousLinearMap.compRingHomCompTriple Β· cited by 234RingHomCompTripleContinuousLinearMapWOT Β· cited by 101ContinuousLinearMapWOTContinuousLinearMapWOT.toCLM Β· cited by 36ContinuousLinearMapWOT.to…ContinuousLinearMapWOT.compCITED BYCITES

Cites9

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

Cited by13

Results whose statement or proof uses this declaration.