finsupp.nonzero_iff_exists

Stream: new members

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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

[Johan Commelin]

Ok, I think both lemmas are useful.

[Johan Commelin]

Note that the first one should be called support_nonempty_iff

[Damiano Testa]

Ok, I will PR both of them, then!

Should they be marked as simp?

[Johan Commelin]

No, I don't think so.

[Johan Commelin]

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

[Damiano Testa]

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]

PR #6530