instZero — Mathlib

English

There is a zero element in C_c(α, β): the zero map with constant value 0 and compact support.

Русский

Существует нулевой элемент в C_c(α, β): нулевое отображение с константным значением 0 и компактной опорой.

LaTeX

$$$ [Zero β] : Zero \big( C_c(α, β) \big)$ defined by 0 := { toFun := (0 : C(α, β)), continuous_toFun := (0 : C(α, β)).2, hasCompactSupport' := by simp [HasCompactSupport, tsupport] }$$

Lean4

instance [Zero β] : Zero C_c(α, β) where
  zero :=
    { toFun := (0 : C(α, β))
      continuous_toFun := (0 : C(α, β)).2
      hasCompactSupport' := by simp [HasCompactSupport, tsupport] }

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