instBoundedContinuousMapClass — Mathlib

English

Defines the class of bounded continuous maps with appropriate map_continuous and map_bounded properties.

Русский

Определяет класс ограниченных непрерывных отображений с заданными свойствами карты.

LaTeX

$$$\\text{BoundedContinuousMapClass } F \\ α β$$$

Lean4

instance instBoundedContinuousMapClass : BoundedContinuousMapClass (α →ᵇ β) α β
    where
  map_continuous f := f.continuous_toFun
  map_bounded f := f.map_bounded'

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