Zulip Chat Archive

Stream: Is there code for X?

Topic: subset of finset is finite


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

view this post on Zulip Johan Commelin (Oct 06 2020 at 04:27):

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

view this post on Zulip Johan Commelin (Oct 06 2020 at 04:27):

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

view this post on Zulip Floris van Doorn (Oct 06 2020 at 04:41):

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

view this post on Zulip Floris van Doorn (Oct 06 2020 at 04:42):

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

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

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

view this post on Zulip Reid Barton (Oct 06 2020 at 13:06):

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

view this post on Zulip Adam Topaz (Oct 06 2020 at 13:12):

Reid Barton said:

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

Looks like I already did.

view this post on Zulip Reid Barton (Oct 06 2020 at 13:15):

Touché


Last updated: May 17 2021 at 16:26 UTC