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

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,
  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: Dec 20 2023 at 11:08 UTC