tendsto_zmultiplesHom_cofinite — Mathlib

English

For a ≠ 0, the map zmultiplesHom(ℝ, a) from ℤ to ℝ is cofinite-to-cocompact.

Русский

Для a ≠ 0 отображение zmultiplesHom(ℝ, a) от ℤ к ℝ кофинитно-кокомпактно.

LaTeX

$$$\\forall a \\in \\mathbb{R}, a \\neq 0 \\Rightarrow \\mathrm{Tendsto}(\\mathrm{zmultiplesHom}\\ \\mathbb{R}\\ a)\\ cofinite\\ (\\mathrm{cocompact}\\ \\mathbb{R})$$$

Lean4

/-- For nonzero `a`, the "multiples of `a`" map `zmultiplesHom` from `ℤ` to `ℝ` is discrete, i.e.
inverse images of compact sets are finite. -/
theorem tendsto_zmultiplesHom_cofinite {a : ℝ} (ha : a ≠ 0) : Tendsto (zmultiplesHom ℝ a) cofinite (cocompact ℝ) :=
  by
  apply (zmultiplesHom ℝ a).tendsto_coe_cofinite_of_discrete <| smul_left_injective ℤ ha
  rw [AddSubgroup.range_zmultiplesHom]
  infer_instance

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