# Zulip Chat Archive

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

s 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):

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

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