instContinuousMapClass

Mathlib.Topology.Algebra.ContinuousAffineMap

URI: https://scilib.ai/kg/mathlib#ContinuousAffineMap.instContinuousMapClass

English

There is an instance ensuring ContinuousAffineMap is a ContinuousMapClass, i.e., its maps are continuous.

Русский

Существуют инстансы, гарантирующие, что ContinuousAffineMap образует ContinuousMapClass, т.е. отображения непрерывны.

LaTeX

$$instance : ContinuousMapClass (P \toᴬ[R] Q) P Q$$

Lean4

instance : ContinuousMapClass (P →ᴬ[R] Q) P Q where map_continuous := cont

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

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

Разделы

Аффилиация

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