ofHom — Mathlib

English

From a continuous linear map one obtains a morphism in TopModuleCat.

Русский

Из непрерывно-линейного отображения получают морфизм в TopModuleCat.

LaTeX

$$$\mathrm{TopModuleCat}.ofHom: f : X \to Y \Rightarrow \mathrm{TopModuleCat}.Hom(X,Y)$$$

Lean4

/-- Construct a hom in `TopModuleCat` from a continuous linear map. -/
abbrev ofHom {X Y : Type v} [AddCommGroup X] [Module R X] [TopologicalSpace X] [ContinuousAdd X] [ContinuousSMul R X]
    [AddCommGroup Y] [Module R Y] [TopologicalSpace Y] [ContinuousAdd Y] [ContinuousSMul R Y] (f : X →L[R] Y) :
    of R X ⟶ of R Y :=
  ConcreteCategory.ofHom f

Похожие утверждения