mem_fundamentalDomain — Mathlib

English

Let b be a basis of E over K. A vector m lies in the fundamental domain of b exactly when all its coordinates with respect to b lie in the half-open interval [0, 1).

Русский

Пусть b — базис пространства E над полем K. Вектор m принадлежит фундаментальной области b тогда и только тогда, когда все координаты m в базисе b лежат в полуинтервале [0, 1).

LaTeX

$$$ m \\in \\operatorname{fundamentalDomain}(b) \\iff \\forall i,\\ b.repr\\,m\\,i \\in [0,1) $$$

Lean4

@[simp]
theorem mem_fundamentalDomain {m : E} : m ∈ fundamentalDomain b ↔ ∀ i, b.repr m i ∈ Set.Ico (0 : K) 1 :=
  Iff.rfl

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