Stream: Is there code for X?

Topic: Finiteness of balls in the integers

Heather Macbeth (Feb 22 2021 at 06:22):

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 (Feb 22 2021 at 06:50):

Using Ico_Z would be my first guess...

Ruben Van de Velde (Feb 22 2021 at 14:16):

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

Ruben Van de Velde (Feb 22 2021 at 14:28):

#6365

Last updated: May 16 2021 at 05:21 UTC