span_latticeBasis — Mathlib

English

The integer lattice in the mixed space carries a discrete topology.

Русский

Целочисленная решётка в смешанном пространстве носит дискретную топологию.

LaTeX

$$$ \text{DiscreteTopology } (mixedEmbedding.integerLattice K) $$$

Lean4

theorem span_latticeBasis : Submodule.span ℤ (Set.range (latticeBasis K)) = mixedEmbedding.integerLattice K :=
  Submodule.ext_iff.mpr fun _ ↦ mem_span_latticeBasis K

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