instContinuousMapClassContMDiffMonoidMorphism

English

Each ContMDiffMonoidMorphism is a continuous map, i.e., its underlying function is continuous.

Русский

Каждый ContMDiffMonoidMorphism является непрерывным отображением, т.е. базовая функция непрерывна.

LaTeX

$$$\\\\forall f: ContMDiffMonoidMorphism I I' n G G', \\\\text{map continuous}(f) $$$

Lean4

@[to_additive]
instance : ContinuousMapClass (ContMDiffMonoidMorphism I I' n G G') G G' where
  map_continuous f := f.contMDiff_toFun.continuous

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