Commit 2025-03-13 06:05 d67fcdf3

feat(Order/Atoms): generalise IsAtomistic typeclass assumptions (#22891) Adjust the IsAtomistic typeclass to assume PartialOrder + OrderBot rather than CompleteLattice. This is a useful change since Finset should be atomistic, but is not a complete lattice in the general case. Add some API lemmas for the new phrasing in terms of IsLUB, and preserve the existing lemmas. Some of the existing instances are also generalised. For convenience, the old IsAtomistic.mk constructor is preserved as CompleteLattice.isAtomistic_iff.2, as the new constructor now has a more general typeclass assumption. This lemma additionally shows that under the old typeclass assumptions, the new and old definitions are equivalent: the mathematical meaning of the typeclass is unchanged. Moves:

• CompleteLattice.isStronglyAtomic -> Lattice.isStronglyAtomic
• CompleteLattice.isStronglyCoatomic -> Lattice.isStronglyCoatomic