restrict_apply — Mathlib

English

For D in LocallyFinsuppWithin, and V ⊆ U, the coefficient of D.restrict h at z equals D z if z ∈ V and 0 otherwise.

Русский

Для D в LocallyFinsuppWithin и V ⊆ U коэффициент (D.restrict h) в точке z равен D(z) если z ∈ V иначе 0.

LaTeX

$$$(D.restrict h)(z) = \\begin{cases} D(z), & z \\in V; \\\\ 0, & z \\notin V. \\end{cases}$$$

Lean4

theorem restrict_apply [Zero Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) (z : X) :
    (D.restrict h) z = if z ∈ V then D z else 0 :=
  rfl

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