Theorems · Inductive type · geometry

ContinuousAffineMap

(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] →
              [Module R V] →
                [TopologicalSpace P] →
                  [AddTorsor V P] →
                    [inst_5 : AddCommGroup W] →
                      [Module R W] → [TopologicalSpace Q] → [AddTorsor W Q] → Type (max (max (max u_2 u_3) u_4) u_5)

A continuous map of affine spaces

Defined in

Mathlib.Topology.Algebra.ContinuousAffineMap

Cited by

263 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 26 definitions · uses no axioms

Assumes

RingAddCommGroupModuleTopologicalSpaceAddTorsorAddCommGroupModuleTopologicalSpaceAddTorsor