instContinuousMapClass — Mathlib

English

An instance making F into a continuous map class between α and β exists when F is a HomeomorphClass.

Русский

Существует экземпляр, делающий F классом непрерывных отображений между α и β, если F — HomeomorphClass.

LaTeX

$$$ \\text{instance }[\\text{HomeomorphClass } F \\alpha \\beta] : ContinuousMapClass F \\alpha \\beta $$$

Lean4

instance [HomeomorphClass F α β] : ContinuousMapClass F α β where map_continuous f := map_continuous f

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