[Merged by Bors] - feat(Order/Atoms): strong atomicity typeclass#14004
[Merged by Bors] - feat(Order/Atoms): strong atomicity typeclass#14004
Conversation
PR summary f4fa74078b
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Order.Atoms.Finite | 488 | 492 | +4 (+0.82%) |
| Mathlib.Order.Atoms | 349 | 351 | +2 (+0.57%) |
| Mathlib.Data.Fintype.Order | 490 | 491 | +1 (+0.20%) |
| Mathlib.GroupTheory.Sylow | 1096 | 1095 | -1 (-0.09%) |
Import changes for all files
| Files | Import difference |
|---|---|
| Too many changes (419)! |
Declarations diff
+ ComplementedLattice.isStronglyAtomic
+ ComplementedLattice.isStronglyAtomic'
+ ComplementedLattice.isStronglyCoatomic
+ ComplementedLattice.isStronglyCoatomic'
+ CompleteLattice.isStronglyAtomic
+ CompleteLattice.isStronglyCoatomic
+ IsStronglyAtomic
+ IsStronglyAtomic.isAtomic
+ IsStronglyAtomic.of_wellFounded_lt
+ IsStronglyCoatomic
+ IsStronglyCoatomic.of_wellFounded_gt
+ IsStronglyCoatomic.toIsCoatomic
+ LT.lt.exists_covby_le
+ LT.lt.exists_le_covby
+ OrderDual.instIsStronglyCoatomic
+ Set.OrdConnected.isStronglyAtomic
+ Set.OrdConnected.isStronglyCoatomic
+ SuccOrder.toIsStronglyAtomic
+ exists_covBy_le_of_lt
+ exists_covby_infinite_Ici_of_infinite_Ici
+ exists_covby_infinite_Iic_of_infinite_Iic
+ exists_le_covBy_of_lt
+ instance : IsStronglyAtomic α
+ instance : IsStronglyCoatomic α := by
+ instance [IsStronglyAtomic α] {s : Set α} [Set.OrdConnected s] : IsStronglyAtomic s
+ instance [IsStronglyCoatomic α] : IsStronglyAtomic αᵒᵈ := by
+ instance [IsStronglyCoatomic α] {s : Set α} [h : Set.OrdConnected s] : IsStronglyCoatomic s
+ instance [PredOrder α] : IsStronglyCoatomic α := by
+ instance [WellFoundedGT α] : IsStronglyCoatomic α
+ instance [WellFoundedLT α] : IsStronglyAtomic α
+ isStronglyAtomic_dual_iff_is_stronglyCoatomic
+ isStronglyCoatomic_dual_iff_is_stronglyAtomic
You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
left a comment
There was a problem hiding this comment.
Rest looks good.
Is “strongly atomic” a concept in the literature? I have never encountered it. Can you either provide a reference or clarify that this is made up for mathlib purposes
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
A quick google search for 'strongly atomic lattice' confirms that the answer is yes, even if it's not so central as a concept. I don't think a citation is needed, any more than one is needed for the existing |
|
Well as a matter of fact I actually think we should document maintainer merge |
|
Well as a matter of fact I actually think we should document Btw your PR description is outdated wrt what's an instance and what's not, I think. maintainer merge |
A strongly atomic preorder is one in which every nontrivial interval `[a,b]` contains an element covering `a`, or equivalently an order where every closed interval is atomic. We add a new typeclass `IsStronglyAtomic` to capture this. We provide instances of this typeclass for `SuccOrder`s, orders with `WellFoundedLT`, atomistic upper-modular lattices, complemented atomic modular lattices, and `OrdConnected` subtypes. We also show that such orders are atomic. We also provide the dual typeclass `IsStronglyCoatomic` and dual versions of all of the above.
|
Pull request successfully merged into master. Build succeeded: |
A strongly atomic preorder is one in which every nontrivial interval
[a,b]contains an element coveringa, or equivalently an order where every closed interval is atomic. We add a new typeclassIsStronglyAtomicto capture this.We provide instances of this typeclass for
SuccOrders, orders withWellFoundedLT, atomistic upper-modular lattices, complemented atomic modular lattices, andOrdConnectedsubtypes. We also show that such orders are atomic.We also provide the dual typeclass
IsStronglyCoatomicand dual versions of all of the above.