Commit 2024-11-04 23:57 dddeda78

View on Github →

chore(SuccPred/Limit): rename 2 lemmas (#18462)

Estimated changes

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem Order.IsPredPrelimit.of_dense

added theorem Order.IsSuccPrelimit.of_dense

deleted theorem Order.isPredPrelimit_of_dense

deleted theorem Order.isSuccPrelimit_of_dense