Zulip Chat Archive

Stream: Is there code for X?

Topic: Finiteness of balls in the integers


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Feb 22 2021 at 06:50):

Using Ico_Z would be my first guess...

view this post on Zulip Adam Topaz (Feb 22 2021 at 14:04):

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

view this post on Zulip 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?

view this post on Zulip Ruben Van de Velde (Feb 22 2021 at 14:28):

#6365


Last updated: May 16 2021 at 05:21 UTC