Finiteness of balls in the integers

Stream: Is there code for X?

[Heather Macbeth]

We seem not to have this?

example (x : ℤ) (r : ℝ) : (metric.closed_ball x r).finite :=

(At least, we don't have its corollary, that ℤ is a docs#proper_space.). I have an ugly proof whose key point is to use docs#finset.Ico_ℤ; is there a better way?

[Johan Commelin]

Using Ico_Z would be my first guess...

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/057997831053da12caf94430419b82b3ac08aec2/src/Mbar/bounded.lean#L18 :smile:

[Ruben Van de Velde]

Oh heh, I thought that reminded me of something. I'll put them in data.fintype.intervals?

[Ruben Van de Velde]

#6365