## Stream: new members

### Topic: finsupp.nonzero_iff_exists

#### Damiano Testa (Mar 04 2021 at 07:48):

Dear All,

is the lemma below already in mathlib? Or can you suggest a better proof, such that I can do directly rcases on the ∃ part, simply feeding it that f is non-zero?

Thanks!

import data.finsupp.basic

lemma finsupp.nonzero_iff_exists {α β : Type*} [has_zero β] {f : finsupp α β} :
f ≠ 0 ↔ ∃ a : α, f a ≠ 0 :=
by simp [finsupp.support_eq_empty.symm, finset.eq_empty_iff_forall_not_mem]


#### Johan Commelin (Mar 04 2021 at 07:51):

@Damiano Testa I guess maybe there should be a support_nonempty_iff lemma?

#### Damiano Testa (Mar 04 2021 at 07:53):

I can find the negation of that statement, but not the direct one...

#### Damiano Testa (Mar 04 2021 at 07:54):

i.e. as you can see, I found support_eq_empty, but not the other one support_nonempty_...

#### Johan Commelin (Mar 04 2021 at 07:56):

Right, because you could do rcases on f.support.nonempty... so it seems useful to have that version as well

#### Johan Commelin (Mar 04 2021 at 07:56):

f.support.nonempty \iff f \ne 0.

#### Damiano Testa (Mar 04 2021 at 08:04):

Ok, so are you suggesting that I should add the first (and maybe also the second) of these lemmas?

/- to add -/
lemma finsupp.nonempty_iff {α β : Type*} [has_zero β] {f : finsupp α β} :
f.support.nonempty ↔ f ≠ 0 :=
by simp only [finsupp.support_eq_empty, finset.nonempty_iff_ne_empty, ne.def]

-- maybe to add
lemma finsupp.nonzero_iff_exists {α β : Type*} [has_zero β] {f : finsupp α β} :
f ≠ 0 ↔ ∃ a : α, f a ≠ 0 :=
by simp [finsupp.support_eq_empty.symm, finset.eq_empty_iff_forall_not_mem]


#### Johan Commelin (Mar 04 2021 at 08:08):

The second is iff.symm of the first, right?

#### Damiano Testa (Mar 04 2021 at 08:11):

Are you suggesting what is below?

lemma finsupp.nonzero_iff_exists {α β : Type*} [has_zero β] {f : finsupp α β} :
f ≠ 0 ↔ ∃ a : α, f a ≠ 0 :=
finsupp.nonempty_iff.symm -- fails
/-
type mismatch, term
finsupp.nonempty_iff.symm
has type
?m_4 ≠ 0 ↔ ?m_4.support.nonempty
but is expected to have type
f ≠ 0 ↔ ∃ (a : α), ⇑f a ≠ 0
-/


#### Johan Commelin (Mar 04 2021 at 08:12):

Ooh, sorry, I'm stupid. Should learn to read.

#### Johan Commelin (Mar 04 2021 at 08:12):

Ok, I think both lemmas are useful.

#### Johan Commelin (Mar 04 2021 at 08:13):

Note that the first one should be called support_nonempty_iff

#### Damiano Testa (Mar 04 2021 at 08:13):

Ok, I will PR both of them, then!

Should they be marked as simp?

#### Johan Commelin (Mar 04 2021 at 08:14):

No, I don't think so.

#### Johan Commelin (Mar 04 2021 at 08:14):

It's not clear to me that they bring things towards some canonical form.

#### Damiano Testa (Mar 04 2021 at 08:15):

Ok, great! Since otherwise, the linter would want me to change the \ne to \not which seems a worse form for the statements!

#### Damiano Testa (Mar 04 2021 at 08:22):

PR #6530

Last updated: May 06 2021 at 21:09 UTC