RootClauseBPayload

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

theorem Algsuperdiff.Section4.Provider.Regularity.offGridLatticeIndex_mem_of_mem_cube {d : ℕ} {m : ℤ} (n : ℤ) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : offGridLatticeIndex n x ∈ Support.latticeCubeSet d n m

The producer's v-binder is met by the root's own x ∈ □_m.