Zulip Chat Archive

Stream: new members

Topic: Non-empty finsets


view this post on Zulip Vincent Beffara (Dec 09 2019 at 14:22):

Hi,

Is this somewhere in mathlib? I feel like I am reinventing the wheel ...

lemma finset.image_ne_empty {V W : Type} [decidable_eq W] {f : V -> W} {A : finset V}
        (h : A  ) : finset.image f A  
    := Exists.dcases_on (finset.exists_mem_of_ne_empty h)
        (λ _, finset.ne_empty_of_mem  finset.mem_image_of_mem f)

view this post on Zulip Johan Commelin (Dec 09 2019 at 15:22):

Not sure if its there, but isn't this mt (finset.image_empty) h, or something like that. (Also, I think in your lemma f should be explicit, since it can't be determined from other variables.

view this post on Zulip Johan Commelin (Dec 09 2019 at 15:29):

Nevermind, I'm talking nonsense with my proof idea.

view this post on Zulip Johan Commelin (Dec 09 2019 at 15:33):

@Vincent Beffara This one looks useful: https://github.com/leanprover-community/mathlib/blob/b031290b228838d5e779908b129420331bb131c5/src/data/finset.lean#L1008

@[simp] theorem image_eq_empty : s.image f =   s =  :=

There is a general way to get the nots into place.

view this post on Zulip Johan Commelin (Dec 09 2019 at 15:36):

I think it's something like not_iff_not_of_iff

view this post on Zulip Mario Carneiro (Dec 09 2019 at 15:46):

oh, I was going to suggest writing that exact statement and calling it image_eq_empty

view this post on Zulip Mario Carneiro (Dec 09 2019 at 15:48):

your proof was just about right too:

lemma finset.image_ne_empty {V W : Type} [decidable_eq W] {f : V -> W} {A : finset V} :
  A    finset.image f A   :=
mt finset.image_eq_empty.1

view this post on Zulip Johan Commelin (Dec 09 2019 at 15:49):

But maybe this statement should also become an iff?

view this post on Zulip Mario Carneiro (Dec 09 2019 at 15:51):

The proof is such that it shouldn't exist at all

view this post on Zulip Vincent Beffara (Dec 09 2019 at 19:35):

Not sure if its there, but isn't this mt (finset.image_empty) h, or something like that.

Ah, right, of course ... I wasn't looking in this direction at all because somehow proving that a set is nonempty by exhibiting an element felt more direct (the proof of image_eq_empty boils down to eq_empty_of_forall_not_mem, eq_zero_of_forall_not_mem, eq_nil_iff_forall_not_mem, eq_nil_of_subset_nil and ultimately false.elim with lots of negatives all over the place).

Thanks!


Last updated: May 13 2021 at 22:15 UTC