Dense orders and finsets

We prove that in a dense order, there's always an element lying in between any two finite sets of elements.

theorem Finset.exists_between {α : Type u_1} [LinearOrder α] [DenselyOrdered α] {s t : Finset α} (hs : s.Nonempty) (ht : t.Nonempty) (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

theorem Finset.exists_between' {α : Type u_1} [LinearOrder α] [DenselyOrdered α] (s t : Finset α) [NoMaxOrder α] [NoMinOrder α] [Nonempty α] (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

theorem Set.Finite.exists_between {α : Type u_1} [LinearOrder α] [DenselyOrdered α] {s t : Set α} (hsf : s.Finite) (hs : s.Nonempty) (htf : t.Finite) (ht : t.Nonempty) (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y

theorem Set.Finite.exists_between' {α : Type u_1} [LinearOrder α] [DenselyOrdered α] [NoMaxOrder α] [NoMinOrder α] [Nonempty α] {s t : Set α} (hs : s.Finite) (ht : t.Finite) (H : ∀ x ∈ s, ∀ y ∈ t, x < y) : ∃ (b : α), (∀ x ∈ s, x < b) ∧ ∀ y ∈ t, b < y