instCoeTCContinuousMap

Mathlib.Topology.ContinuousMap.Defs

URI: https://scilib.ai/kg/mathlib#instCoeTCContinuousMap

English

There is a canonical coercion from F to C(X,Y) given by the map f ↦ toContinuousMap(f).

Русский

Существует каноническое приведение типов из F в C(X,Y), отображающее f в toContinuousMap(f).

LaTeX

$$f \\mapsto toContinuousMap(f)$$

Lean4

instance : CoeTC F C(X, Y) :=
  ⟨toContinuousMap⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru