instNeg — Mathlib

English

The zero-at-infinity maps form an additive group: there is a negation (-f) defined pointwise by (-f)(x) = -f(x).

Русский

Множество отображений с нулём при бесконечности образует группу по сложению; разность задаётся по точкам: (-f)(x) = -f(x).

LaTeX

$$C₀(α, β) is an AddGroup with (-f)(x) = -f(x).$$

Lean4

instance instNeg : Neg C₀(α, β) :=
  ⟨fun f => ⟨-f, by simpa only [neg_zero] using (zero_at_infty f).neg⟩⟩

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