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.