feat(Data/Multiset/Powerset): show injectivity and monotonicity of powerset#35465
feat(Data/Multiset/Powerset): show injectivity and monotonicity of powerset#35465MixedMatched wants to merge 3 commits intoleanprover-community:masterfrom
Conversation
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary a90320db82
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.List.Sublists | 298 | 299 | +1 (+0.34%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Data.List.Sublists |
1 |
Declarations diff
+ Subperm.append
+ Subperm.map
+ le_powerset_iff_le
+ powerset_eq_singleton_empty_iff
+ powerset_injective
+ powerset_mono
+ powerset_strictMono
+ self_mem_powerset
+ sublists'_subperm_sublists'
+ zero_mem_powerset
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for scripts/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
| theorem Subperm.append {l₁ l₂ r₁ r₂ : List α} | ||
| (hl : l₁.Subperm l₂) (hr : r₁.Subperm r₂) : | ||
| (l₁ ++ r₁).Subperm (l₂ ++ r₂) := by | ||
| obtain ⟨l, hl_perm, hl_sub⟩ := hl | ||
| obtain ⟨r, hr_perm, hr_sub⟩ := hr | ||
| exact ⟨l ++ r, hl_perm.append hr_perm, hl_sub.append hr_sub⟩ |
There was a problem hiding this comment.
Perhaps tidier as
| theorem Subperm.append {l₁ l₂ r₁ r₂ : List α} | |
| (hl : l₁.Subperm l₂) (hr : r₁.Subperm r₂) : | |
| (l₁ ++ r₁).Subperm (l₂ ++ r₂) := by | |
| obtain ⟨l, hl_perm, hl_sub⟩ := hl | |
| obtain ⟨r, hr_perm, hr_sub⟩ := hr | |
| exact ⟨l ++ r, hl_perm.append hr_perm, hl_sub.append hr_sub⟩ | |
| theorem Subperm.append {l₁ l₂ r₁ r₂ : List α} : | |
| l₁ <+~ l₂ → r₁ <+~ r₂ → (l₁ ++ r₁) <+~ (l₂ ++ r₂) | |
| | ⟨l, hl_perm, hl_sub⟩, ⟨r, hr_perm, hr_sub⟩ => | |
| ⟨l ++ r, hl_perm.append hr_perm, hl_sub.append hr_sub⟩ |
| (h : l₁.Subperm l₂) : | ||
| (l₁.map f).Subperm (l₂.map f) := by |
There was a problem hiding this comment.
This one should also prefer the <+~ notation
| @@ -354,6 +355,18 @@ theorem sublists_perm_sublists' (l : List α) : sublists l ~ sublists' l := by | |||
| · exact nodup_sublists.mpr (nodup_finRange _) | |||
| · exact (nodup_sublists'.mpr (nodup_finRange _)) | |||
|
|
|||
| theorem sublists'_subperm_sublists' {l₁ l₂ : List α} | |||
| (sublist : l₁.Sublist l₂) : | |||
| l₁.sublists'.Subperm l₂.sublists' := by | |||
There was a problem hiding this comment.
This is true more generally as
| l₁.sublists'.Subperm l₂.sublists' := by | |
| l₁.sublists'.Sublist l₂.sublists' := by |
and the theorem should be called Sublist.sublists'
| @[simp] | ||
| theorem card_powerset (s : Multiset α) : card (powerset s) = 2 ^ card s := | ||
| Quotient.inductionOn s <| by simp | ||
|
|
||
| theorem powerset_eq_singleton_empty_iff (s) : @powerset α s = {0} ↔ s = 0 where |
There was a problem hiding this comment.
| theorem powerset_eq_singleton_empty_iff (s) : @powerset α s = {0} ↔ s = 0 where | |
| theorem powerset_eq_singleton_zero_iff (s) : @powerset α s = {0} ↔ s = 0 where |
this also looks like a good simp lemma.
| lemma powerset_mono : Monotone (@Multiset.powerset α) := by | ||
| unfold Monotone | ||
| intro a₁ a₂ a | ||
| exact le_powerset_iff_le.mpr a | ||
|
|
||
| lemma powerset_injective : Function.Injective (@Multiset.powerset α) := by | ||
| unfold Function.Injective | ||
| intro a₁ a₂ a | ||
| exact le_antisymm | ||
| (le_powerset_iff_le.mp (le_of_eq a)) | ||
| (le_powerset_iff_le.mp (le_of_eq a.symm)) | ||
|
|
||
| lemma powerset_strictMono : StrictMono (@Multiset.powerset α) := by | ||
| exact Monotone.strictMono_of_injective powerset_mono powerset_injective |
There was a problem hiding this comment.
I think you can get here faster with strictMono_of_le_iff_le
| @@ -146,6 +159,29 @@ theorem revzip_powersetAux_perm {l₁ l₂ : List α} (p : l₁ ~ l₂) : | |||
| simp only [fun l : List α => revzip_powersetAux_lemma l revzip_powersetAux, coe_eq_coe.2 p] | |||
| exact (powersetAux_perm p).map _ | |||
|
|
|||
| theorem le_powerset_iff_le {s t} : | |||
There was a problem hiding this comment.
| theorem le_powerset_iff_le {s t} : | |
| theorem powerset_le_powerset_iff_le {s t} : |
| @@ -104,10 +104,23 @@ theorem map_single_le_powerset (s : Multiset α) : s.map singleton ≤ powerset | |||
| rw [← List.map_map] | |||
| exact ((map_pure_sublist_sublists _).map _).subperm | |||
|
|
|||
| theorem zero_mem_powerset (s) : 0 ∈ @powerset α s := | |||
|
Thanks for spotting these gaps in mathlib! |
Add Injective, Monotone, and StrictMono proofs for
Multiset.powerset. Also, add a theorem showing that the sizes of two powersets are bidirectionally related to the sizes of the underlying Multisets (le_powerset_iff_le), a couple of other smallMultiset.powersetlemmas, and theorems for append and map forList.Subperm.Also, thanks to Ruben Van de Velde for looking this over on the Zulip!