set.finite of subset range

Stream: Is there code for X?

[Damiano Testa]

Dear All,

I do not know my way at all around finite, finset, fintype, so I am hoping that the lemma below is easy to prove! Can anyone suggest a way to make progress on this?

Bonus: I would be particularly grateful for an answer that teaches me how to solve this kind of questions without bothering the Zulip crowd!

Thanks!

import data.finset.basic
import data.set.finite

lemma set.finite_of_finset_range {s : set ℕ} (d : ℕ) (sd : s ⊆ finset.range d) :
  s.finite :=
begin
  sorry,
end

[Eric Wieser]

Does docs#set.finite.mono exist?

[Damiano Testa]

Your link sends to a 404...

[Damiano Testa]

I tried looking for some form of mono, but I could not find it (which does not mean that it does not exist, of course!).

[Eric Wieser]

docs#set.finite.subset?

[Damiano Testa]

Ah, this one exists, let me try!

[Damiano Testa]

Great, this works! Thanks!

lemma set.finite_of_finset_range {s : set ℕ} (d : ℕ) (sd : s ⊆ finset.range d) :
  s.finite :=
(range d).finite_to_set.subset sd