∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : SemilatticeInf Y] [inst_2 : Zero Y]
  (D₁ D₂ : Function.locallyFinsuppWithin U Y), ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support fun z => D₁ z ⊓ D₂ z).Finite