Commit 2024-04-04 21:40 8a2f1006

View on Github →

style: fix references to DenselyOrdered (#11897) Rename occurrences of "densely_ordered" to "denselyOrdered"

Estimated changes

Modified Mathlib/Data/PSigma/Order.lean

Modified Mathlib/Order/CountableDenseLinearOrder.lean

Modified Mathlib/Order/Cover.lean

added theorem denselyOrdered_iff_forall_not_covBy

deleted theorem densely_ordered_iff_forall_not_covBy