[Merged by Bors] - feat(SetTheory/ZFC/Basic): order instances#19946
[Merged by Bors] - feat(SetTheory/ZFC/Basic): order instances#19946
Conversation
PR summary 132d7a7b21
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.SetTheory.ZFC.Basic | 391 | 393 | +2 (+0.51%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.SetTheory.ZFC.Basic |
2 |
Declarations diff
+ instance : HasSSubset PSet := ⟨(· < ·)⟩
+ instance : HasSSubset ZFSet := ⟨(· < ·)⟩
+ instance : IsNonstrictStrictOrder PSet (· ⊆ ·) (· ⊂ ·)
+ instance : IsNonstrictStrictOrder ZFSet (· ⊆ ·) (· ⊂ ·)
+ instance : Preorder PSet
+ instance : SetLike ZFSet ZFSet
++ le_def
++ lt_def
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 script/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).
alreadydone
left a comment
There was a problem hiding this comment.
Thanks!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
alreadydone
left a comment
There was a problem hiding this comment.
Apparently we can introduce a SetLike instance (on ZFSet, not on PSet) and then the PartialOrder from SetLike.instPartialOrder is defeq to this. (There's a PR that demotes SetLike.instPartialOrder from an instance to an abbrev (I suppose) though.)
|
I guess you're right... ZFC sets are in fact kind of like sets :P I'll rework this PR to implement that instance instead. |
|
Thanks |
|
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
Sets form a partial order under the subset relation.
|
Pull request successfully merged into master. Build succeeded: |
Sets form a partial order under the subset relation.
Sets form a partial order under the subset relation.
Sets form a partial order under the subset relation.