Mathlib Map

Theorems Β· Definition Β· functional analysis

ContinuousLinearEquiv.arrowCongrSL

{π•œ : Type u_1} β†’
  {π•œβ‚‚ : Type u_2} β†’
    {π•œβ‚ƒ : Type u_3} β†’
      {π•œβ‚„ : Type u_4} β†’
        {E : Type u_5} β†’
          {F : Type u_6} β†’
            {G : Type u_7} β†’
              {H : Type u_8} β†’
                [inst : AddCommGroup E] β†’
                  [inst_1 : AddCommGroup F] β†’
                    [inst_2 : AddCommGroup G] β†’
                      [inst_3 : AddCommGroup H] β†’
                        [inst_4 : NormedField π•œ] β†’
                          [inst_5 : NormedField π•œβ‚‚] β†’
                            [inst_6 : NormedField π•œβ‚ƒ] β†’
                              [inst_7 : NormedField π•œβ‚„] β†’
                                [inst_8 : Module π•œ E] β†’
                                  [inst_9 : Module π•œβ‚‚ F] β†’
                                    [inst_10 : Module π•œβ‚ƒ G] β†’
                                      [inst_11 : Module π•œβ‚„ H] β†’
                                        [inst_12 : TopologicalSpace E] β†’
                                          [inst_13 : TopologicalSpace F] β†’
                                            [inst_14 : TopologicalSpace G] β†’
                                              [inst_15 : TopologicalSpace H] β†’
                                                [inst_16 : IsTopologicalAddGroup G] β†’
                                                  [inst_17 : IsTopologicalAddGroup H] β†’
                                                    [inst_18 : ContinuousConstSMul π•œβ‚ƒ G] β†’
                                                      [inst_19 : ContinuousConstSMul π•œβ‚„ H] β†’
                                                        {σ₁₂ : π•œ β†’+* π•œβ‚‚} β†’
                                                          {σ₂₁ : π•œβ‚‚ β†’+* π•œ} β†’
                                                            {σ₂₃ : π•œβ‚‚ β†’+* π•œβ‚ƒ} β†’
                                                              {σ₁₃ : π•œ β†’+* π•œβ‚ƒ} β†’
                                                                {σ₃₄ : π•œβ‚ƒ β†’+* π•œβ‚„} β†’
                                                                  {σ₄₃ : π•œβ‚„ β†’+* π•œβ‚ƒ} β†’
                                                                    {Οƒβ‚‚β‚„ : π•œβ‚‚ β†’+* π•œβ‚„} β†’
                                                                      {σ₁₄ : π•œ β†’+* π•œβ‚„} β†’
                                                                        [inst_20 : RingHomInvPair σ₁₂ σ₂₁] β†’
                                                                          [inst_21 : RingHomInvPair σ₂₁ σ₁₂] β†’
                                                                            [inst_22 : RingHomInvPair σ₃₄ σ₄₃] β†’
                                                                              [inst_23 : RingHomInvPair σ₄₃ σ₃₄] β†’
                                                                                [RingHomCompTriple σ₂₁ σ₁₄ Οƒβ‚‚β‚„] β†’
                                                                                  [RingHomCompTriple Οƒβ‚‚β‚„ σ₄₃ σ₂₃] β†’
                                                                                    [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] β†’
                                                                                      [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] β†’
                                                                                        [RingHomCompTriple σ₂₃ σ₃₄
                                                                                              Οƒβ‚‚β‚„] β†’
                                                                                          [RingHomCompTriple σ₁₂ Οƒβ‚‚β‚„
                                                                                                σ₁₄] β†’
                                                                                            [RingHomIsometric σ₁₂] β†’
                                                                                              [RingHomIsometric σ₂₁] β†’
                                                                                                (E ≃SL[σ₁₂] F) β†’
                                                                                                  (H ≃SL[σ₄₃] G) β†’
                                                                                                    β‹― ≃SL[σ₄₃] β‹―

A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the spaces of continuous (semi)linear maps.

Defined in
Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
Cited by
6 results in Mathlib
Foundations
Depth 159 from the axioms Β· uses propext, Classical.choice, Quot.sound
Assumes
AddCommGroupAddCommGroupAddCommGroupAddCommGroupNormedFieldNormedFieldNormedFieldNormedFieldModuleModuleModuleModuleTopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceIsTopologicalAddGroupIsTopologicalAddGroupContinuousConstSMulContinuousConstSMulRingHomInvPairRingHomInvPairRingHomInvPairRingHomInvPairRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomCompTripleRingHomIsometricRingHomIsometric
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ContinuousLinearEquiv.arrowCongr Β· cited by 16ContinuousLinearEquiv.arr…Bundle.Pretrivialization.continuousLinearMapCoordChange Β· cited by 5Pretrivialization.continu…ContinuousLinearEquiv.arrowCongrSL_apply Β· cited by 2ContinuousLinearEquiv.arr…tendsto_integral_exp_smul_cocompact Β· cited by 1tendsto_integral_exp_smul…ContinuousLinearEquiv.arrowCongrSL_symm_apply Β· cited by 0ContinuousLinearEquiv.arr…ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_apply Β· cited by 0ContinuousLinearEquiv.arr…ContinuousLinearEquiv.arrowCongrSL_toLinearEquiv_symm_apply Β· cited by 0ContinuousLinearEquiv.arr…ContinuousLinearEquiv.arrowCongrSL.congr_simp Β· cited by 0arrowCongrSL.congr_simpTopologicalSpace Β· cited by 24529TopologicalSpaceModule Β· cited by 20661ModuleAddCommGroup Β· cited by 12871AddCommGroupRingHom Β· cited by 10189RingHomContinuousLinearMap Β· cited by 5352ContinuousLinearMapLinearEquiv Β· cited by 3317LinearEquivIsTopologicalAddGroup Β· cited by 1394IsTopologicalAddGroupNormedField Β· cited by 1084NormedFieldContinuousConstSMul Β· cited by 832ContinuousConstSMulContinuousLinearEquiv Β· cited by 743ContinuousLinearEquivContinuousLinearMap.comp Β· cited by 709ContinuousLinearMap.compRingHomInvPair Β· cited by 523RingHomInvPairContinuousLinearEquiv.toContinuousLinearMap Β· cited by 448ContinuousLinearEquiv.toC…ContinuousLinearEquiv.symm Β· cited by 368ContinuousLinearEquiv.symmRingHomIsometric Β· cited by 282RingHomIsometricContinuousLinearEquiv.arrowCo…CITED BYCITES

Cites17

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

Cited by8

Results whose statement or proof uses this declaration.