Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(data/finsupp/basic): add support_nonempty_iff and nonzero_iff_exists #6530

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(data/finsupp/basic): add support_nonempty_iff and nonzero_iff_exists #6530

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions src/data/finsupp/basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -147,6 +147,12 @@ lemma ext_iff' {f g : α →₀ M} : f = g ↔ f.support = g.support ∧ ∀ x
⟨assume h, ext $ assume a, by_contradiction $ λ H, (finset.ext_iff.1 h a).1 $
mem_support_iff.2 H, by rintro rfl; refl⟩

lemma support_nonempty_iff {f : α →₀ M} : f.support.nonempty ↔ f ≠ 0 :=
by simp only [finsupp.support_eq_empty, finset.nonempty_iff_ne_empty, ne.def]

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]
Comment on lines +153 to +154
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we have this statement somewhere?

lemma pi.nonzero_iff_exists {f : α → M} : f ≠ 0 ↔ ∃ a : α, f a ≠ 0 :=
sorry

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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, ...

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is #4985 all over again, of course.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member

@eric-wieser eric-wieser Mar 4, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Definitely no need to grow this PR :)


lemma card_support_eq_zero {f : α →₀ M} : card f.support = 0 ↔ f = 0 :=
by simp

Expand Down