fundamentalDomain_subset_parallelepiped

English

The fundamental domain is contained in the parallelepiped generated by the basis b.

Русский

Фундаментальная область содержится в параллелепипеде, порождаемом базисом b.

LaTeX

$$$\operatorname{fundamentalDomain}(b) \subseteq \operatorname{parallelepiped}(b).$$$

Lean4

theorem fundamentalDomain_subset_parallelepiped [Fintype ι] : fundamentalDomain b ⊆ parallelepiped b :=
  by
  rw [fundamentalDomain, parallelepiped_basis_eq, Set.setOf_subset_setOf]
  exact fun _ h i ↦ Set.Ico_subset_Icc_self (h i)

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