quotientEquiv_apply_mk — Mathlib

English

For a finite index set ι and any x ∈ E, there exists a unique v ∈ spanℤ(range b) such that v +ᵥ x ∈ fundamentalDomain b.

Русский

Для каждого x ∈ E существует единственный v ∈ spanℤ(range b), для которого v +ᵥ x принадлежит fundamentalDomain(b).

LaTeX

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

Lean4

@[simp]
theorem quotientEquiv_apply_mk [Fintype ι] (x : E) : quotientEquiv b (Submodule.Quotient.mk x) = fractRestrict b x :=
  rfl

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