Theorems · Theorem · order theory

Order.exists_between_finsets

∀ {α : Type u_1} [inst : LinearOrder α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [nonem : Nonempty α]
  (lo hi : Finset α), (∀ x ∈ lo, ∀ y ∈ hi, x < y) → ∃ m, (∀ x ∈ lo, x < m) ∧ ∀ y ∈ hi, m < y

Suppose α is a nonempty dense linear order without endpoints, and suppose lo, hi, are finite subsets with all of lo strictly before hi. Then there is an element of α strictly between lo and hi.

Defined in

Mathlib.Order.CountableDenseLinearOrder

Cited by

2 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderDenselyOrderedNoMinOrderNoMaxOrderNonempty