tendsto_zmultiples_subtype_cofinite

English

The subgroup of multiples a in ℝ, as a Subgroup, is discrete: the subtype map has cofinite-to-cocompact tendsto.

Русский

Подгруппа кратных a в ℝ дискретна: отображение подмодуля имеет стремление кофинитно к кокопмактной топологии.

LaTeX

$$$\\operatorname{Tendsto}((\\mathrm{zmultiples}\, a).\\mathrm{subtype})\\;\\text{cofinite}\\; (\\mathrm{cocompact}\\ Real)$$$

Lean4

/-- The subgroup "multiples of `a`" (`zmultiples a`) is a discrete subgroup of `ℝ`, i.e. its
intersection with compact sets is finite. -/
theorem tendsto_zmultiples_subtype_cofinite (a : ℝ) : Tendsto (zmultiples a).subtype cofinite (cocompact ℝ) :=
  (zmultiples a).tendsto_coe_cofinite_of_discrete

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