Non-empty finsets

Stream: new members

[Vincent Beffara]

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]

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]

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

[Johan Commelin]

@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]

I think it's something like not_iff_not_of_iff

[Mario Carneiro]

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

[Mario Carneiro]

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]

But maybe this statement should also become an iff?

[Mario Carneiro]

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

[Vincent Beffara]

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!