apply_eq_zero_of_notMem — Mathlib

English

If z is not in U, then any locally finite function within U evaluates to zero at z.

Русский

Если z не принадлежит U, то локально конечное внутри U функция принимает значение 0 в z.

LaTeX

$$$\\forall z \\notin U,\\ D(z)=0$$$

Lean4

/-- Simplifier lemma: Functions with locally finite support within `U` evaluate to zero outside of `U`.
-/
@[simp]
theorem apply_eq_zero_of_notMem [Zero Y] {z : X} (D : locallyFinsuppWithin U Y) (hz : z ∉ U) : D z = 0 :=
  notMem_support.mp fun a ↦ hz (D.supportWithinDomain a)

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