## Stream: Is there code for X?

### Topic: subset of finset is finite

#### Adam Topaz (Oct 06 2020 at 04:13):

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 (Oct 06 2020 at 04:27):

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

#### Johan Commelin (Oct 06 2020 at 04:27):

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

#### Floris van Doorn (Oct 06 2020 at 04:41):

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

#### Floris van Doorn (Oct 06 2020 at 04:42):

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

#### Kyle Miller (Oct 06 2020 at 06:04):

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 (Oct 06 2020 at 12:52):

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

#### Adam Topaz (Oct 06 2020 at 13:12):

Reid Barton said:

#### Reid Barton (Oct 06 2020 at 13:15):

Touché

Last updated: May 17 2021 at 16:26 UTC