tendsto_coe_cofinite — Mathlib

English

For real a ≠ 0, the map zmultiplesHom(a): ℤ → ℝ is cofinite-to-cocompact (discrete image).

Русский

Для действительного a ≠ 0 отображение zmultiplesHom(a): ℤ → ℝ — кофинитно-кокомпактно.

LaTeX

$$$\\text{Tendsto}(\\mathrm{zmultiplesHom}\\ \\mathbb{R}\\ a)\\ cofinite\\ (\\mathrm{cocompact}\\ \\mathbb{R})$, если a \\neq 0$$

Lean4

/-- Under the coercion from `ℤ` to `ℝ`, inverse images of compact sets are finite. -/
theorem tendsto_coe_cofinite : Tendsto ((↑) : ℤ → ℝ) cofinite (cocompact ℝ) :=
  by
  apply (castAddHom ℝ).tendsto_coe_cofinite_of_discrete cast_injective
  rw [range_castAddHom]
  infer_instance

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