[Merged by Bors] - feat(data/finsupp/basic): add support_nonempty_iff and nonzero_iff_exists #6530
Conversation
adomani
added
the
awaiting-review
github-actions
bot
added
ready-to-merge
| lemma nonzero_iff_exists {f : α →₀ M} : f ≠ 0 ↔ ∃ a : α, f a ≠ 0 := | ||
| by simp [finsupp.support_eq_empty.symm, finset.eq_empty_iff_forall_not_mem] |
There was a problem hiding this comment.
Do we have this statement somewhere?
lemma pi.nonzero_iff_exists {f : α → M} : f ≠ 0 ↔ ∃ a : α, f a ≠ 0 :=
sorryThere was a problem hiding this comment.
And also add_monoid_hom.nonzero_iff_exists, monoid_hom.nonzero_iff_exists, ring_hom.nonzero_iff_exists, linear_map.nonzero_iff_exists, alg_hom.nonzero_iff_exists, ...
There was a problem hiding this comment.
This is #4985 all over again, of course.
There was a problem hiding this comment.
I do not know if these are there, but if you do not know about them, then I doubt it!
In any case, I do not know what the namespace pi stands for: is it a synonym for set?
There was a problem hiding this comment.
pi is the type of dependent functions - both of these can be thought of as pi types:
variables (α : Sort*) (β : α → Sort*) (γ : Sort*)
#check (Π a, β a)
#check (Π a : α, γ) -- aka α → γMathlib is inconsistent when it comes to using the pi and function namespaces.
There was a problem hiding this comment.
Note that if you prove the pi version, finsupp.nonzero_iff_exists becomes simply coe_fn_injective.eq_iff.trans the_pi_version, possibly with some .symms
There was a problem hiding this comment.
Eric, thank you for explaining the pi stuff!
While I understand that these pi lemmas should be there as well, I am not sure that I am willing to risk another growth of this PR like what happened in the past! Would it be ok if I left it at that? Maybe this issue can go in a TODO list?
There was a problem hiding this comment.
Definitely no need to grow this PR :)
…ists (#6530) Add two lemmas to work with `finsupp`s with non-empty support. Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/finsupp.2Enonzero_iff_exists
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
…ists (#6530) Add two lemmas to work with `finsupp`s with non-empty support. Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/finsupp.2Enonzero_iff_exists
Add two lemmas to work with
finsupps with non-empty support.Zulip:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/finsupp.2Enonzero_iff_exists