style: fix references to DenselyOrdered (#11897)

Rename occurrences of "densely_ordered" to "denselyOrdered"



Co-authored-by: sven-manthe <147848313+sven-manthe@users.noreply.github.com>

Mathlib/Data/PSigma/Order.lean

@@ -153,15 +153,15 @@ instance denselyOrdered_of_noMaxOrder [Preorder ι] [∀ i, Preorder (α i)]
       exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩⟩
 #align psigma.lex.densely_ordered_of_no_max_order PSigma.Lex.denselyOrdered_of_noMaxOrder
 
-instance densely_ordered_of_noMinOrder [Preorder ι] [∀ i, Preorder (α i)]
+instance denselyOrdered_of_noMinOrder [Preorder ι] [∀ i, Preorder (α i)]
     [∀ i, DenselyOrdered (α i)] [∀ i, NoMinOrder (α i)] : DenselyOrdered (Σₗ' i, α i) :=
   ⟨by
     rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)
     · obtain ⟨c, hb⟩ := exists_lt b
       exact ⟨⟨j, c⟩, left _ _ h, right _ hb⟩
     · obtain ⟨c, ha, hb⟩ := exists_between h
       exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩⟩
-#align psigma.lex.densely_ordered_of_no_min_order PSigma.Lex.densely_ordered_of_noMinOrder
+#align psigma.lex.densely_ordered_of_no_min_order PSigma.Lex.denselyOrdered_of_noMinOrder
 
 instance noMaxOrder_of_nonempty [Preorder ι] [∀ i, Preorder (α i)] [NoMaxOrder ι]
     [∀ i, Nonempty (α i)] : NoMaxOrder (Σₗ' i, α i) :=

Mathlib/Order/CountableDenseLinearOrder.lean

@@ -46,7 +46,7 @@ theorem exists_between_finsets {α : Type*} [LinearOrder α] [DenselyOrdered α]
     ∃ m : α, (∀ x ∈ lo, x < m) ∧ ∀ y ∈ hi, m < y :=
   if nlo : lo.Nonempty then
     if nhi : hi.Nonempty then
-      -- both sets are nonempty, use densely_ordered
+      -- both sets are nonempty, use `DenselyOrdered`
         Exists.elim
         (exists_between (lo_lt_hi _ (Finset.max'_mem _ nlo) _ (Finset.min'_mem _ nhi))) fun m hm ↦
         ⟨m, fun x hx ↦ lt_of_le_of_lt (Finset.le_max' lo x hx) hm.1, fun y hy ↦
@@ -61,7 +61,7 @@ theorem exists_between_finsets {α : Type*} [LinearOrder α] [DenselyOrdered α]
         Exists.elim
         (exists_lt (Finset.min' hi nhi)) fun m hm ↦
         ⟨m, fun x hx ↦ (nlo ⟨x, hx⟩).elim, fun y hy ↦ lt_of_lt_of_le hm (Finset.min'_le hi y hy)⟩
-    else-- both sets are empty, use nonempty
+    else -- both sets are empty, use `Nonempty`
           nonem.elim
         fun m ↦ ⟨m, fun x hx ↦ (nlo ⟨x, hx⟩).elim, fun y hy ↦ (nhi ⟨y, hy⟩).elim⟩
 #align order.exists_between_finsets Order.exists_between_finsets

Mathlib/Order/Cover.lean

@@ -245,10 +245,12 @@ theorem not_covBy [DenselyOrdered α] : ¬a ⋖ b := fun h =>
   h.2 hc.1 hc.2
 #align not_covby not_covBy
 
-theorem densely_ordered_iff_forall_not_covBy : DenselyOrdered α ↔ ∀ a b : α, ¬a ⋖ b :=
+theorem denselyOrdered_iff_forall_not_covBy : DenselyOrdered α ↔ ∀ a b : α, ¬a ⋖ b :=
   ⟨fun h _ _ => @not_covBy _ _ _ _ h, fun h =>
     ⟨fun _ _ hab => exists_lt_lt_of_not_covBy hab <| h _ _⟩⟩
-#align densely_ordered_iff_forall_not_covby densely_ordered_iff_forall_not_covBy
+@[deprecated] alias densely_ordered_iff_forall_not_covBy :=
+  denselyOrdered_iff_forall_not_covBy -- 2024-04-04
+#align densely_ordered_iff_forall_not_covby denselyOrdered_iff_forall_not_covBy
 
 @[simp]
 theorem toDual_covBy_toDual_iff : toDual b ⋖ toDual a ↔ a ⋖ b :=