coe_zero — Mathlib

English

Let Y be an additive abelian group and X a topological space with U a subset of X. The zero element of the space of locally finitely supported Y-valued functions on U corresponds to the identically zero function on X.

Русский

Пусть Y — абелева группа, X — топологическое пространство, U ⊆ X. Нуль-элемент пространства функций с локально конечной поддержкой в U соответствует тождественной нулевой функции на X.

LaTeX

$$$((0 : \\text{locallyFinsuppWithin}(U,Y)) : X \\to Y) = 0$$$

Lean4

@[simp]
theorem coe_zero [AddCommGroup Y] : ((0 : locallyFinsuppWithin U Y) : X → Y) = 0 :=
  rfl

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