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

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

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

source
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.

source
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.

source
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.