subset of finset is finite

Stream: Is there code for X?

[Adam Topaz]

Is something similar to this in mathlib?

import data.finset
example {α : Type*} (S : set α) (F : finset α) : S ⊆ ↑F → ∃ G : finset α, ↑G = S := sorry

[Johan Commelin]

I think if you use set.finite the machinery is there.

[Johan Commelin]

@Adam Topaz it might even fit on 1 line (-;

[Floris van Doorn]

More specifically, use docs#set.finite.subset and docs#set.finite.to_finset

[Floris van Doorn]

Oh, and docs#finset.finite_to_set to get the exact statement

[Kyle Miller]

There's also set.to_finset:

def fintype_subset_finset (s : set α) {t : set α} [fintype s] [decidable_pred t] (h : t ⊆ s) : finset α :=
@set.to_finset α t (fintype_subset s h)

example (t : set α) (s : finset α) (h : t ⊆ ↑s) : ∃ t' : finset α, ↑t' = t :=
begin
  classical,
  use fintype_subset_finset ↑s h,
  simp [fintype_subset_finset],
end

[Adam Topaz]

Ugh, do I really have to combine three different mathlib lemmas to get such a simple thing!?

[Reid Barton]

Sign my petition at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/finiteness/near/206179081

[Adam Topaz]

Reid Barton said:

Sign my petition at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/finiteness/near/206179081

Looks like I already did.

[Reid Barton]

Touché