exist_unique_vadd_mem_fundamentalDomain

English

For finite ι and any x in E, there exists a unique v in spanℤ(range b) such that v added to x lies in the fundamental domain.

Русский

Для конечного ι и любого x в E существует единственный элемент v ∈ spanℤ(range b), для которого x+cидит в фундаментальную область.

LaTeX

$$$\exists! v \in \operatorname{span}_{\mathbb{Z}}(\operatorname{range} b): v + x \in \operatorname{fundamentalDomain}(b).$$$

Lean4

theorem exist_unique_vadd_mem_fundamentalDomain [Finite ι] (x : E) :
    ∃! v : span ℤ (Set.range b), v +ᵥ x ∈ fundamentalDomain b :=
  by
  cases nonempty_fintype ι
  refine ⟨-floor b x, ?_, fun y h => ?_⟩
  · exact (vadd_mem_fundamentalDomain b (-floor b x) x).mpr rfl
  · exact (vadd_mem_fundamentalDomain b y x).mp h

Похожие утверждения