∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommGroup Y] [inst_2 : Lattice Y]
  {V : Set X} (h : V ⊆ U) (D₁ D₂ : Function.locallyFinsuppWithin U Y),
  (D₁ ⊓ D₂).restrict h = D₁.restrict h ⊓ D₂.restrict h