English
Restriction maps a function with locally finite support on U to a function with locally finite support on a subset V ⊆ U by sending values outside V to zero.
Русский
Ограничение переводит функцию с локальной конечной поддержкой на U в функцию на подмножестве V ⊆ U, нули вне V задаются нулём.
LaTeX
$$$\\text{restrict} : (\\text{locallyFinsuppWithin } U Y) \\to (\\text{locallyFinsuppWithin } V Y)$, defined by (toFun z) = if z ∈ V then D z else 0$$
Lean4
/-- If `V` is a subset of `U`, then functions with locally finite support within `U` restrict to
functions with locally finite support within `V`, by setting their values to zero outside of `V`.
-/
noncomputable def restrict [Zero Y] {V : Set X} (D : locallyFinsuppWithin U Y) (h : V ⊆ U) : locallyFinsuppWithin V Y
where
toFun := by classical exact fun z ↦ if hz : z ∈ V then D z else 0
supportWithinDomain' := by
intro x hx
simp_rw [dite_eq_ite, mem_support, ne_eq, ite_eq_right_iff, Classical.not_imp] at hx
exact hx.1
supportLocallyFiniteWithinDomain' := by
intro z hz
obtain ⟨t, ht⟩ := D.supportLocallyFiniteWithinDomain z (h hz)
use t, ht.1
apply Set.Finite.subset (s := t ∩ D.support) ht.2
intro _ _
simp_all
