exists_between_finsets — Mathlib

English

In a densely ordered, non-endpoint linear order without endpoints, given two finite sets lo and hi with all elements of lo strictly less than all elements of hi, there exists an element strictly between lo and hi.

Русский

В плотно упорядоченном линейном порядке без пределов существует элемент между двумя данными конечными множествами, если каждый элемент lo меньше любого элемента hi.

LaTeX

$$$\\text{Let } \\alpha \\text{ be a densely ordered linear order without endpoints. For finite sets } LO, HI, \\forall x\\in LO, \\forall y\\in HI, x

Lean4

/-- 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`. -/
theorem exists_between_finsets [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [nonem : Nonempty α] (lo hi : Finset α)
    (lo_lt_hi : ∀ x ∈ lo, ∀ y ∈ hi, x < y) : ∃ m : α, (∀ x ∈ lo, x < m) ∧ ∀ y ∈ hi, m < y :=
  if nlo : lo.Nonempty then
    if nhi : hi.Nonempty then
        -- 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 ↦
          lt_of_lt_of_le hm.2 (Finset.min'_le hi y hy)⟩
    else -- upper set is empty, use `NoMaxOrder`
      Exists.elim (exists_gt (Finset.max' lo nlo)) fun m hm ↦
        ⟨m, fun x hx ↦ lt_of_le_of_lt (Finset.le_max' lo x hx) hm, fun y hy ↦ (nhi ⟨y, hy⟩).elim⟩
  else
    if nhi : hi.Nonempty then
        -- lower set is empty, use `NoMinOrder`

      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`
      nonem.elim fun m ↦ ⟨m, fun x hx ↦ (nlo ⟨x, hx⟩).elim, fun y hy ↦ (nhi ⟨y, hy⟩).elim⟩

Похожие утверждения