Theorems · Definition · geometry

ContinuousAffineMap.decompLinearEquiv

(R : Type u_1) →
  (S : Type u_2) →
    (V : Type u_3) →
      (W : Type u_4) →
        [inst : Ring S] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : Module R V] →
                [inst_4 : TopologicalSpace V] →
                  [IsTopologicalAddGroup V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : Module R W] →
                        [inst_8 : TopologicalSpace W] →
                          [inst_9 : Module S W] →
                            [inst_10 : SMulCommClass R S W] →
                              [inst_11 : ContinuousConstSMul S W] →
                                [inst_12 : IsTopologicalAddGroup W] → (V →ᴬ[R] W) ≃ₗ[S] W × (V →L[R] W)

The space of continuous affine maps between topological vector spaces is linearly isomorphic to the product of the codomain with the space of linear maps, by taking the value of the affine map at (0 : V) and the linear part.

Defined in

Mathlib.Topology.Algebra.ContinuousAffineMap

Cited by

7 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingRingAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupAddCommGroupModuleTopologicalSpaceModuleSMulCommClassContinuousConstSMulIsTopologicalAddGroup