Multiples of a real number form a discrete subgroup of ℝ

The subgroup "multiples of a" (zmultiples a) is a discrete subgroup of ℝ, i.e. its intersection with compact sets is finite.

instance Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples {a : ℝ} : DiscreteTopology ↥(AddSubgroup.zmultiples a)

This is a special case of NormedSpace.discreteTopology_zmultiples. It exists only to simplify dependencies.

theorem Int.tendsto_coe_cofinite : Filter.Tendsto Int.cast Filter.cofinite (Filter.cocompact ℝ)

Under the coercion from ℤ to ℝ, inverse images of compact sets are finite.

theorem Int.tendsto_zmultiplesHom_cofinite {a : ℝ} (ha : a ≠ 0) : Filter.Tendsto (⇑((zmultiplesHom ℝ) a)) Filter.cofinite (Filter.cocompact ℝ)

For nonzero a, the "multiples of a" map zmultiplesHom from ℤ to ℝ is discrete, i.e. inverse images of compact sets are finite.

theorem AddSubgroup.tendsto_zmultiples_subtype_cofinite (a : ℝ) : Filter.Tendsto (⇑(zmultiples a).subtype) Filter.cofinite (Filter.cocompact ℝ)

The subgroup "multiples of a" (zmultiples a) is a discrete subgroup of ℝ, i.e. its intersection with compact sets is finite.