English
For a finite index set ι and any y in the Z-span of the basis range, and any x in E, y translated by x lies in the fundamental domain exactly when y equals the negative floor of x with respect to b.
Русский
Для конечного множества индексов ι и любого y∈spanℤ(range b), а также для любого x∈E, перенос y на x лежит в фундаментальной области тогда и только тогда, когда y = − floor b x.
LaTeX
$$$\forall y \in \operatorname{span}_{\mathbb{Z}}(\operatorname{range} b),\forall x\in E:\ (y+ x) \in \operatorname{fundamentalDomain}(b) \iff y = -\lfloor b x\rfloor.$$$
Lean4
theorem vadd_mem_fundamentalDomain [Fintype ι] (y : span ℤ (Set.range b)) (x : E) :
y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x := by
rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply, ←
fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ← fract_eq_self]
