## Stream: new members

### Topic: Non-empty finsets

#### 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)


#### 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.

#### Johan Commelin (Dec 09 2019 at 15:29):

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

#### 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.

#### Johan Commelin (Dec 09 2019 at 15:36):

I think it's something like not_iff_not_of_iff

#### Mario Carneiro (Dec 09 2019 at 15:46):

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

#### Mario Carneiro (Dec 09 2019 at 15:48):

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


#### Johan Commelin (Dec 09 2019 at 15:49):

But maybe this statement should also become an iff?

#### Mario Carneiro (Dec 09 2019 at 15:51):

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

#### 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