Z is discrete

Stream: Is there code for X?

[Adam Topaz]

Do we have a lemma approximately like the following?

import analysis.normed_space.basic

example (n : ℤ) : ∥ n ∥ < 1 → n = 0 := sorry

[Ruben Van de Velde]

example (n : ℤ) : ∥ n ∥ < 1 → n = 0 := by {
  rw int.norm_eq_abs,
  norm_cast,
  exact int.eq_zero_iff_abs_lt_one.mp
}

[Patrick Massot]

maybe we should have a library_search_mod_cast :wink:

[Adam Topaz]

thanks @Ruben Van de Velde !

[Heather Macbeth]

FWIW, I have found docs#int.tendsto_coe_cofinite to be a useful abstract formulation of "ℤ is discrete":

/-- Under the coercion from `ℤ` to `ℝ`, inverse images of compact sets are finite. -/
lemma tendsto_coe_cofinite : tendsto (coe : ℤ → ℝ) cofinite (cocompact ℝ) :=

[Kevin Buzzard]

This is a lovely way of thinking about it! Actually it would look even nicer using ideals not filters because then the co- prefixes would go