instAddZeroClassOfContinuousAdd — Mathlib

English

If β is AddZeroClass and ContinuousAdd, then C_c(α,β) inherits an AddZeroClass structure, with addition and zero defined pointwise. In particular, the zero map has compact support and f+0=f=0+f for all f.

Русский

Если β имеет AddZeroClass и ContinuousAdd, то C_c(α,β) наследует структуру AddZeroClass, где сложение и ноль выполняются по точкам; нулевая функция имеет компактную опору и для всех f выполняется f+0=f=0+f.

LaTeX

$$$$ f+0 = f \quad\text{and}\quad 0+f = f \quad\text{for all } f \in C_c(\alpha,\beta). $$$$

Lean4

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

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