Zulip Chat Archive

Stream: new members

Topic: finsupp.nonzero_iff_exists


view this post on Zulip 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]

view this post on Zulip Johan Commelin (Mar 04 2021 at 07:51):

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

view this post on Zulip Damiano Testa (Mar 04 2021 at 07:53):

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

view this post on Zulip 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_...

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 04 2021 at 07:56):

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

view this post on Zulip 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]

view this post on Zulip Johan Commelin (Mar 04 2021 at 08:08):

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

view this post on Zulip 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
-/

view this post on Zulip Johan Commelin (Mar 04 2021 at 08:12):

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

view this post on Zulip Johan Commelin (Mar 04 2021 at 08:12):

Ok, I think both lemmas are useful.

view this post on Zulip Johan Commelin (Mar 04 2021 at 08:13):

Note that the first one should be called support_nonempty_iff

view this post on Zulip Damiano Testa (Mar 04 2021 at 08:13):

Ok, I will PR both of them, then!

Should they be marked as simp?

view this post on Zulip Johan Commelin (Mar 04 2021 at 08:14):

No, I don't think so.

view this post on Zulip Johan Commelin (Mar 04 2021 at 08:14):

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

view this post on Zulip 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!

view this post on Zulip Damiano Testa (Mar 04 2021 at 08:22):

PR #6530


Last updated: May 06 2021 at 21:09 UTC