From 4d861b0a62bd07f6c88aa1816fea1d7bfffbb3ca Mon Sep 17 00:00:00 2001 From: sven-manthe <147848313+sven-manthe@users.noreply.github.com> Date: Thu, 4 Apr 2024 20:28:15 +0200 Subject: [PATCH] Update Mathlib/Order/CountableDenseLinearOrder.lean Co-authored-by: grunweg --- Mathlib/Order/CountableDenseLinearOrder.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/CountableDenseLinearOrder.lean b/Mathlib/Order/CountableDenseLinearOrder.lean index 0084e3c6964c5..6b2beabcf0b55 100644 --- a/Mathlib/Order/CountableDenseLinearOrder.lean +++ b/Mathlib/Order/CountableDenseLinearOrder.lean @@ -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