instAddConstMapClass — Mathlib

English

The space G →+c[a, b] H carries its own AddConstMapClass structure, i.e., the class lifts to the space of constant-mapped functions.

Русский

Множество функций G →+c[a,b] H наследует структуру AddConstMapClass, т.е. класс поднимается на пространство константных отображений.

LaTeX

$$$\text{AddConstMapClass} (G \to\!+c[a,b] H) \; G \; H \; a \; b$$$

Lean4

instance : AddConstMapClass (G →+c[a, b] H) G H a b where map_add_const f := f.map_add_const'

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