instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite

English

The Z-span lattice Submodule(span ℤ (range b)) defines a discrete subgroup in E.

Русский

Латтьице Z-порождает подгруппу в E, которая дискретна.

LaTeX

$$$\operatorname{DiscreteTopology}(\operatorname{span}_{\mathbb{Z}}(\operatorname{range} b)).$$$

Lean4

instance [Finite ι] : DiscreteTopology (span ℤ (Set.range b)) :=
  by
  have h : Set.MapsTo b.equivFun (span ℤ (Set.range b)) (span ℤ (Set.range (Pi.basisFun ℝ ι))) :=
    by
    intro _ hx
    rwa [SetLike.mem_coe, Basis.mem_span_iff_repr_mem] at hx ⊢
  convert DiscreteTopology.of_continuous_injective ((continuous_equivFun_basis b).restrict h) ?_
  · exact discreteTopology_pi_basisFun
  · refine Subtype.map_injective _ (Basis.equivFun b).injective

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