Theorems · Definition · geometry

ContinuousAffineMap.noConfusionType

Sort u →
  {R : Type u_1} →
    {V : Type u_2} →
      {W : Type u_3} →
        {P : Type u_4} →
          {Q : Type u_5} →
            [inst : Ring R] →
              [inst_1 : AddCommGroup V] →
                [inst_2 : Module R V] →
                  [inst_3 : TopologicalSpace P] →
                    [inst_4 : AddTorsor V P] →
                      [inst_5 : AddCommGroup W] →
                        [inst_6 : Module R W] →
                          [inst_7 : TopologicalSpace Q] →
                            [inst_8 : AddTorsor W Q] →
                              (P →ᴬ[R] Q) →
                                {R' : Type u_1} →
                                  {V' : Type u_2} →
                                    {W' : Type u_3} →
                                      {P' : Type u_4} →
                                        {Q' : Type u_5} →
                                          [inst' : Ring R'] →
                                            [inst'_1 : AddCommGroup V'] →
                                              [inst'_2 : Module R' V'] →
                                                [inst'_3 : TopologicalSpace P'] →
                                                  [inst'_4 : AddTorsor V' P'] →
                                                    [inst'_5 : AddCommGroup W'] →
                                                      [inst'_6 : Module R' W'] →
                                                        [inst'_7 : TopologicalSpace Q'] →
                                                          [inst'_8 : AddTorsor W' Q'] → (P' →ᴬ[R'] Q') → Sort u

Defined in

Mathlib.Topology.Algebra.ContinuousAffineMap

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

RingAddCommGroupModuleTopologicalSpaceAddTorsorAddCommGroupModuleTopologicalSpaceAddTorsorRingAddCommGroupModuleTopologicalSpaceAddTorsorAddCommGroupModuleTopologicalSpaceAddTorsor