# Zulip Chat Archive

## 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

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

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):

#### 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,
simp [int.lt_add_one_iff],
end
example (r : ℝ) : set.finite { x : ℤ | abs (x : ℝ) ≤ r } :=
begin
convert Icc_finite _ _,
ext,
rw [←int.cast_abs, ←le_floor, abs_le],
end
```

Last updated: May 19 2021 at 00:40 UTC