fundamentalDomain_isBounded — Mathlib

English

Let E be a normed vector space over a normed field K, with a basis b indexed by a finite set ι. Then the fundamental domain associated to b is a bounded subset of E.

Русский

Пусть E — нормированное векторное пространство над нормированным полем K, задан базис b, индексируемый конечным множеством ι. Тогда фундаментальная область, связанная с b, ограничена в E.

LaTeX

$$$\operatorname{IsBounded}(\operatorname{fundamentalDomain}(b)).$$$

Lean4

theorem fundamentalDomain_isBounded [Finite ι] [HasSolidNorm K] : IsBounded (fundamentalDomain b) :=
  by
  cases nonempty_fintype ι
  refine isBounded_iff_forall_norm_le.2 ⟨∑ j, ‖b j‖, fun x hx ↦ ?_⟩
  rw [← fract_eq_self.mpr hx]
  apply norm_fract_le

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