Theorems · Theorem · geometry

ContinuousAffineMap.decompAffineEquiv_symm_contLinear

∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : 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 : AddTorsor W Q]
  [inst_13 : TopologicalSpace Q] [inst_14 : IsTopologicalAddGroup W] [inst_15 : IsTopologicalAddTorsor Q]
  (p : Q × (V →L[R] W)), ((ContinuousAffineMap.decompAffineEquiv R S V Q).symm p).contLinear = p.2

Defined in

Mathlib.Topology.Algebra.ContinuousAffineMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingRingAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupAddCommGroupModuleTopologicalSpaceModuleSMulCommClassContinuousConstSMulAddTorsorTopologicalSpaceIsTopologicalAddGroupIsTopologicalAddTorsor