instAddZeroClass

Mathlib.Topology.ContinuousMap.ZeroAtInfty

URI: https://scilib.ai/kg/mathlib#ZeroAtInftyContinuousMap.instAddZeroClass

English

The coercion map from C₀(α,β) to α→β is injective.

Русский

Коercion-проекция из C₀(α,β) в α→β инъективна.

LaTeX

$$$ \text{Injective } (\,f \mapsto f) $$$

Lean4

instance instAddZeroClass [AddZeroClass β] [ContinuousAdd β] : AddZeroClass C₀(α, β) :=
  DFunLike.coe_injective.addZeroClass _ coe_zero coe_add

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

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

Разделы

Аффилиация

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