## Stream: Is there code for X?

### Topic: A bounded set of integers is finite

#### Adam Topaz (Dec 10 2020 at 17:10):

I'm sure we have this somewhere....

example (r : ℝ) : set.finite { x : ℤ | abs (x : ℝ) ≤ r } := sorry


#### Ruben Van de Velde (Dec 10 2020 at 19:16):

I reduced to example (a b : ℤ) : set.finite (Icc a b) := sorry, but that doesn't seem to be there either

#### Adam Topaz (Dec 10 2020 at 19:18):

I've been trying to use the fact that $\mathbb{Z}$ is discrete, that $[a,b]$ is coompact in $\mathbb{R}$ (which is in mathlib), and the fact that a compact subspace of a discrete space is finite. But it looks like mathlib doesn't have embedding (coe : \Z \to \R)...

#### Adam Topaz (Dec 10 2020 at 19:19):

But there is an "easy" list we can write down that enumerates all elements of Icc a b for integers a b, so maybe it's not too bad?

#### Reid Barton (Dec 10 2020 at 19:22):

This definitely sounds like overkill

I know....

#### Reid Barton (Dec 10 2020 at 19:23):

Ruben's suggestion sounds like the right way

#### Adam Topaz (Dec 10 2020 at 19:23):

I'm just trying to find the shortest proof with what's currently in mathlib...

#### Ruben Van de Velde (Dec 10 2020 at 19:23):

I don't know where to go from there, sadly

#### Reid Barton (Dec 10 2020 at 19:24):

I guess define an injective function into fin (b - a + 1)

#### Adam Topaz (Dec 10 2020 at 19:25):

or a surjective function from fin ...

#### Adam Topaz (Dec 10 2020 at 19:27):

@Reid Barton We will definitely want the (topological) embedding of $\mathbb{Z}$ into $\mathbb{R}$ at some point anyway...

#### Patrick Massot (Dec 10 2020 at 19:39):

We definitely have this somewhere.

#### Adam Topaz (Dec 10 2020 at 19:39):

@Patrick Massot you mean the embedding? That would be great!

#### Patrick Massot (Dec 10 2020 at 19:41):

Otherwise interval_cases couldn't do its magic.

#### Patrick Massot (Dec 10 2020 at 19:41):

I mean finiteness of intervals in $\mathbb Z$

#### Adam Topaz (Dec 10 2020 at 19:41):

Oh. Even that would be great :)

#### Reid Barton (Dec 10 2020 at 19:42):

actually I'm not sure why I thought Adam's approach was so overkill

#### Adam Topaz (Dec 10 2020 at 19:42):

You have to prove discreteness somehow...

#### Reid Barton (Dec 10 2020 at 19:42):

as long as you don't think too hard about the proof of compactness

#### Adam Topaz (Dec 10 2020 at 19:42):

compactness of the real closed intervals is in mathlib... zero thinking :)

#### Patrick Massot (Dec 10 2020 at 19:43):

docs#set.Ico_ℤ_fintype

#### Ruben Van de Velde (Dec 10 2020 at 21:11):

import data.fintype.intervals
import data.set.intervals.basic
import data.real.basic

open set

lemma Ico_finite (a b : ℤ) : set.finite (Ico a b) := ⟨set.Ico_ℤ_fintype a b⟩
lemma Icc_finite (a b : ℤ) : set.finite (Icc a b) :=
begin
by_cases h : b < a,
{ convert finite_empty,
exact Icc_eq_empty h },
push_neg at h,
rw ←set.Ico_union_right h,
exact finite.union (Ico_finite a b) (finite_singleton b),
end

example (r : ℝ) : set.finite { x : ℤ | abs (x : ℝ) ≤ r } :=
begin
convert Icc_finite _ _,
ext,
rw [←int.cast_abs, ←le_floor, abs_le],
end


#### Yury G. Kudryashov (Dec 10 2020 at 22:09):

For Icc_finite you can also convert it to Ico_finite a (b + 1).

#### Adam Topaz (Dec 11 2020 at 00:19):

A little golfing following @Yury G. Kudryashov 's suggestion:

import data.fintype.intervals
import data.set.intervals.basic
import data.real.basic

open set

lemma Ico_finite (a b : ℤ) : set.finite (Ico a b) := ⟨set.Ico_ℤ_fintype a b⟩
lemma Icc_finite (a b : ℤ) : set.finite (Icc a b) :=
begin
convert Ico_finite a (b+1),
ext,