instContinuousMapClass — Mathlib

English

The structure C(X,Y) inherits a ContinuousMapClass, where the map_continuous component is taken from the underlying continuous-ness of maps.

Русский

Структура C(X,Y) наследует ContinuousMapClass, где компонент map_continuous берётся из непрерывности отображений.

LaTeX

$$$[ContinuousMapClass\\; C(X,Y)\\; X\\; Y]$ with $map\\_continuous := ContinuousMap.continuous\\_toFun$$$

Lean4

instance instContinuousMapClass : ContinuousMapClass C(X, Y) X Y where map_continuous := ContinuousMap.continuous_toFun

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