Zulip Chat Archive

Stream: Is there code for X?

Topic: A bounded set of integers is finite


view this post on Zulip Adam Topaz (Dec 10 2020 at 17:10):

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

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

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

view this post on Zulip Adam Topaz (Dec 10 2020 at 19:18):

I've been trying to use the fact that Z\mathbb{Z} is discrete, that [a,b][a,b] is coompact in R\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)...

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

view this post on Zulip Reid Barton (Dec 10 2020 at 19:22):

This definitely sounds like overkill

view this post on Zulip Adam Topaz (Dec 10 2020 at 19:23):

I know....

view this post on Zulip Reid Barton (Dec 10 2020 at 19:23):

Ruben's suggestion sounds like the right way

view this post on Zulip Adam Topaz (Dec 10 2020 at 19:23):

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

view this post on Zulip Ruben Van de Velde (Dec 10 2020 at 19:23):

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

view this post on Zulip Reid Barton (Dec 10 2020 at 19:24):

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

view this post on Zulip Adam Topaz (Dec 10 2020 at 19:25):

or a surjective function from fin ...

view this post on Zulip Adam Topaz (Dec 10 2020 at 19:27):

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

view this post on Zulip Patrick Massot (Dec 10 2020 at 19:39):

We definitely have this somewhere.

view this post on Zulip Adam Topaz (Dec 10 2020 at 19:39):

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

view this post on Zulip Patrick Massot (Dec 10 2020 at 19:41):

Otherwise interval_cases couldn't do its magic.

view this post on Zulip Patrick Massot (Dec 10 2020 at 19:41):

I mean finiteness of intervals in Z\mathbb Z

view this post on Zulip Adam Topaz (Dec 10 2020 at 19:41):

Oh. Even that would be great :)

view this post on Zulip Reid Barton (Dec 10 2020 at 19:42):

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

view this post on Zulip Adam Topaz (Dec 10 2020 at 19:42):

You have to prove discreteness somehow...

view this post on Zulip Reid Barton (Dec 10 2020 at 19:42):

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

view this post on Zulip Adam Topaz (Dec 10 2020 at 19:42):

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

view this post on Zulip Patrick Massot (Dec 10 2020 at 19:43):

docs#set.Ico_ℤ_fintype

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

view this post on Zulip Yury G. Kudryashov (Dec 10 2020 at 22:09):

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

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