chore(Data/Finset/Lattice/Fold): rename comp_sup_* to apply_sup_*#37185
chore(Data/Finset/Lattice/Fold): rename comp_sup_* to apply_sup_*#37185gasparattila wants to merge 5 commits intoleanprover-community:masterfrom
comp_sup_* to apply_sup_*#37185Conversation
This PR uses the `@[to_dual]` attribute to generate dual lemmas about `Finset.sup`. The lemmas about `sdiff` and `himp` are skipped, as `HeytingAlgebra` is not yet tagged with `@[to_dual]`. Other changes: - tag `inf_insert` with `@[grind =]` - rename `le_inf_const_le` to `le_inf_const` - tag `inf_union` with `@[grind _=_]` - tag `inf_mono_fun` with `@[grind ←]` - tag `inf_mono` with `@[grind ←]` - tag `inf_attach` with `@[simp]` - add `le_inf_of_directed_le` - add `inf_eq_top_of_isEmpty` - add `inf_mem_of_nonempty` - rename `comp_sup_eq_sup_comp_of_is_total` to `comp_sup_eq_sup_comp_of_linearOrder` (and similarly for the `inf` version) - add `inf'_mono_fun` - add `comp_inf_eq_inf_comp_of_nonempty`
PR summary 49ba224813Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 8395 | -2 | backward.isDefEq |
Current commit 1245092d60
Reference commit 49ba224813
You can run this locally as
./scripts/reporting/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).
|
This PR/issue depends on:
|
These lemmas are of the form `g (s.sup f) = s.sup (g ∘ f)` with no composition on the LHS.
a0058ce to
1245092
Compare
These lemmas are of the form
g (s.sup f) = s.sup (g ∘ f)with no composition on the LHS.to_dual#37047