Basic order theorems

theorem not_le_of_le_of_not_le {α : Type u_1} [Preorder α] {a b c : α} (h₁ : a ≤ b) (h₂ : ¬c ≤ b) : ¬c ≤ a

theorem not_le_of_not_le_of_le {α : Type u_1} [Preorder α] {a b c : α} (h₁ : ¬b ≤ a) (h₂ : b ≤ c) : ¬c ≤ a

theorem not_lt_of_antisymmRel {α : Type u_1} [Preorder α] {x y : α} (h : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) x y) : ¬x < y

theorem not_gt_of_antisymmRel {α : Type u_1} [Preorder α] {x y : α} (h : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) x y) : ¬y < x

theorem AntisymmRel.not_lt {α : Type u_1} [Preorder α] {x y : α} (h : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) x y) : ¬x < y

Alias of not_lt_of_antisymmRel.

theorem AntisymmRel.not_gt {α : Type u_1} [Preorder α] {x y : α} (h : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) x y) : ¬y < x

Alias of not_gt_of_antisymmRel.

theorem not_antisymmRel_of_lt {α : Type u_1} [Preorder α] {x y : α} : x < y → ¬AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) x y

theorem not_antisymmRel_of_gt {α : Type u_1} [Preorder α] {x y : α} : y < x → ¬AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) x y

theorem LT.lt.not_antisymmRel {α : Type u_1} [Preorder α] {x y : α} : x < y → ¬AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) x y

Alias of not_antisymmRel_of_lt.

theorem LT.lt.not_antisymmRel_symm {α : Type u_1} [Preorder α] {x y : α} : y < x → ¬AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) x y

Alias of not_antisymmRel_of_gt.

exists_between for Finsets

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