Zulip Chat Archive

Stream: new members

Topic: subset from finset declaration


view this post on Zulip Manuel Candales (Apr 14 2021 at 01:49):

I am defining a finset like: {e ∈ finset.range n | 2 ∣ e }, and I want to show that it is a subset of finset.range

import data.finset

example (n : ) (M : finset  := {e  finset.range n | 2  e }) : M  finset.range n :=
begin
  sorry,
end

I tried simp, dsimp, hint, library_search, suggest. Nothing worked.
I tried defining M using finset.filter as follows, to then apply finset.filter_subset.

import data.finset

example (n : ) (p :   Prop := (λ e, 2  e)) (M : finset  := finset.filter p (finset.range n)) :
  M  finset.range n :=
begin
  sorry,
end

But this is giving me an error, asking for ⊢ decidable_pred p.
Could someone please point me in the right direction?

view this post on Zulip Yakov Pechersky (Apr 14 2021 at 01:59):

example (n : ) (p :   Prop) (hp : p = λ e, 2  e) [decidable_pred p] (M : finset )
  (hM : M = finset.filter p (finset.range n)) :
  M  finset.range n :=
begin
  rw hM,
  exact finset.filter_subset p _,
end

view this post on Zulip Yakov Pechersky (Apr 14 2021 at 01:59):

Or write open_locale classical

open_locale classical

example (n : ) (p :   Prop) (hp : p = λ e, 2  e) (M : finset )
  (hM : M = finset.filter p (finset.range n)) :
  M  finset.range n :=
begin
  rw hM,
  exact finset.filter_subset p _,
end

view this post on Zulip Yakov Pechersky (Apr 14 2021 at 02:00):

example (n : ) (M : finset )
  (hM : M = finset.filter (λ e, 2  e) (finset.range n)) :
  M  finset.range n :=
begin
  rw hM,
  exact finset.filter_subset _ _,
end

view this post on Zulip Yakov Pechersky (Apr 14 2021 at 02:01):

When you say what p is equal to in a separate hypothesis, that doesn't let the finset.filter in the body of the lemma/example statement know that it is decidable.

view this post on Zulip Manuel Candales (Apr 14 2021 at 02:19):

Thank you! open_locale classical helped!


Last updated: May 10 2021 at 19:16 UTC