instAddGroup — Mathlib

English

If β is an AddGroup with IsTopologicalAddGroup, then C_c(α,β) carries an AddGroup structure with pointwise operations.

Русский

Если β имеет AddGroup и IsTopologicalAddGroup, то C_c(α,β) обладает структурой AddGroup с операциями по точкам.

LaTeX

$$$$ (f+g) = h, \ f,g,h ∈ C_c(α,β) $$$$

Lean4

instance : AddGroup C_c(α, β) :=
  DFunLike.coe_injective.addGroup _ coe_zero coe_add coe_neg coe_sub (fun _ _ => rfl) fun _ _ => rfl

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