instIsZLatticeRealSpan — Mathlib

English

If L is a lattice and discrete topology is assumed, then L is finite as a module over the integers.

Русский

Если L — решётка и задана дискретная топология, то L конечно как модуль над целыми числами.

LaTeX

$$$\text{Module.Finite}_{\mathbb{Z}}(L).$$$

Lean4

instance instIsZLatticeRealSpan {E ι : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [Finite ι] (b : Basis ι ℝ E) :
    IsZLattice ℝ (span ℤ (Set.range b)) where span_top := ZSpan.span_top b

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