covolume_ne_zero — Mathlib

English

The covolume of a lattice L with respect to μ is nonzero; in particular, the fundamental domain has positive measure.

Русский

Коволюм решетки L относительно μ не равен нулю; следовательно, фундаментальная область имеет положительную меру.

LaTeX

$$$\\operatorname{covolume}(L,\\mu) \\neq 0$$$

Lean4

theorem covolume_ne_zero : covolume L μ ≠ 0 :=
  by
  rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain (Free.chooseBasis ℤ L) μ),
    measureReal_ne_zero_iff (ne_of_lt _)]
  · exact measure_fundamentalDomain_ne_zero _
  · exact Bornology.IsBounded.measure_lt_top (fundamentalDomain_isBounded _)

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