Statement file: IsZ2Periodic (Roots). This file contains exactly one declaration of the formalization's public statement surface.

def AVenhance.IsZ2Periodic {β : Type u_1} (f : Homogenization.Vec 2 → β) : Prop

ℤ²-periodicity: f (x + n) = f x for all n ∈ ℤ², x ∈ ℝ².

Equations

• AVenhance.IsZ2Periodic f = ∀ (n : Fin 2 → ℤ) (x : Homogenization.Vec 2), f (x + AVenhance.latticeShift n) = f x