Theorems · Theorem · geometry

ContinuousAffineMap.mk.inj

∀ {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} {toAffineMap : P →ᵃ[R] Q}
  {cont : Continuous toAffineMap.toFun} {toAffineMap_1 : P →ᵃ[R] Q} {cont_1 : Continuous toAffineMap_1.toFun},
  { toAffineMap := toAffineMap, cont := cont } = { toAffineMap := toAffineMap_1, cont := cont_1 } →
    toAffineMap = toAffineMap_1

Defined in

Mathlib.Topology.Algebra.ContinuousAffineMap

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms