class TotalOrder (α : Type u_3) extends PartialOrder α : Type u_3

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_total : ∀ (x y : α), Comparable x y

class IsTotalOrder {α : Type u_1} (r : Relation α α) extends IsPartialOrder r : Prop

• le_refl : ∀ (a : α), (a, a) ∈ r
• le_trans : ∀ (a b c : α), (a, b) ∈ r → (b, c) ∈ r → (a, c) ∈ r
• le_antisymm : ∀ (a b : α), (a, b) ∈ r → (b, a) ∈ r → a = b
• le_total : ∀ (a b : α), (a, b) ∈ r ∨ (b, a) ∈ r

instance instTotalOrderRelAsLEOfIsTotalOrder {α : Type u_1} {r : Relation α α} [inst : IsTotalOrder r] : TotalOrder (RelAsLE r)

Equations

• instTotalOrderRelAsLEOfIsTotalOrder = TotalOrder.mk ⋯

theorem TotalOrder.isTotalOrder {α : Type u_1} [TotalOrder α] : IsTotalOrder {p : α × α | p.fst ≤ p.snd}

theorem le_total {α : Type u_1} [TotalOrder α] (x y : α) : x ≤ y ∨ y ≤ x

theorem lt_trichotomy {α : Type u_1} [TotalOrder α] (x y : α) : x < y ∨ x = y ∨ y < x

theorem not_ge_iff_lt {α : Type u_1} {x y : α} [TotalOrder α] : ¬y ≤ x ↔ x < y

theorem not_gt_iff_le {α : Type u_1} {x y : α} [TotalOrder α] : ¬y < x ↔ x ≤ y

theorem le_of_not_ge {α : Type u_1} {x y : α} [TotalOrder α] (h : ¬y ≤ x) : x ≤ y

noncomputable instance instMaxOfTotalOrder {α : Type u_1} [TotalOrder α] : Max α

Equations

• instMaxOfTotalOrder = { max := fun (x y : α) => if x ≤ y then y else x }

@[simp]

theorem max_eq_left_iff {α : Type u_1} {x y : α} [TotalOrder α] : x ⊔ y = y ↔ x ≤ y

@[simp]

theorem max_eq_right_iff {α : Type u_1} {x y : α} [TotalOrder α] : x ⊔ y = x ↔ y ≤ x

theorem max_eq_either {α : Type u_1} [TotalOrder α] (x y : α) : x ⊔ y = x ∨ x ⊔ y = y

noncomputable instance instMinOfTotalOrder {α : Type u_1} [TotalOrder α] : Min α

Equations

• instMinOfTotalOrder = { min := fun (x y : α) => if x ≤ y then x else y }

@[simp]

theorem min_eq_left_iff {α : Type u_1} {x y : α} [TotalOrder α] : x ⊓ y = y ↔ y ≤ x

@[simp]

theorem min_eq_right_iff {α : Type u_1} {x y : α} [TotalOrder α] : x ⊓ y = x ↔ x ≤ y

theorem min_eq_either {α : Type u_1} [TotalOrder α] (x y : α) : x ⊔ y = x ∨ x ⊔ y = y

noncomputable instance instLatticeOfTotalOrder {α : Type u_1} [TotalOrder α] : Lattice α

Equations

• instLatticeOfTotalOrder = Lattice.mk max ⋯ ⋯ ⋯

instance instTotalOrderSubtype {α : Type u_1} [TotalOrder α] {p : α → Prop} : TotalOrder { x : α // p x }

Equations

• instTotalOrderSubtype = TotalOrder.mk ⋯

instance instTotalOrderOfSubsingleton {α : Type u_1} [Subsingleton α] : TotalOrder α

Equations

• instTotalOrderOfSubsingleton = TotalOrder.mk ⋯

instance instTotalOrderOp {α : Type u_1} [TotalOrder α] : TotalOrder (Op α)

Equations

• instTotalOrderOp = TotalOrder.mk ⋯

def TotalOrder.of_surjective_monotone {α : Type u_1} {β : Type u_2} [TotalOrder α] [PartialOrder β] {f : α → β} (h : Monotone f) (h' : Function.Surjective f) : TotalOrder β

Equations

• TotalOrder.of_surjective_monotone h h' = TotalOrder.mk ⋯

theorem TotalOrder.inj_of_strictMono {α : Type u_1} {β : Type u_2} [TotalOrder α] [Preorder β] {f : α → β} (h : StrictMonotone f) : Function.Injective f

theorem TotalOrder.inj_of_strictAnti {α : Type u_1} {β : Type u_2} [TotalOrder α] [Preorder β] {f : α → β} (h : StrictAntitone f) : Function.Injective f

theorem TotalOrder.strictMono_reflect {α : Type u_1} {β : Type u_2} {x y : α} [TotalOrder α] [PartialOrder β] {f : α → β} (h : StrictMonotone f) : f x ≤ f y → x ≤ y

theorem TotalOrder.mono_lt_reflect {α : Type u_1} {β : Type u_2} {x y : α} [TotalOrder α] [PartialOrder β] {f : α → β} (h : Monotone f) : f x < f y → x < y

theorem TotalOrder.strictMono_le_iff {α : Type u_1} {β : Type u_2} {x y : α} [TotalOrder α] [PartialOrder β] {f : α → β} (h : StrictMonotone f) : f x ≤ f y ↔ x ≤ y

theorem TotalOrder.strictMono_iso_image {α : Type u_1} {β : Type u_2} [TotalOrder α] [PartialOrder β] {f : α → β} (h : StrictMonotone f) (h' : Function.Surjective f) : IsOrderIso f

theorem TotalOrder.corestrict_strictMono_iso {α : Type u_1} {β : Type u_2} [TotalOrder α] [PartialOrder β] {f : α → β} (h : StrictMonotone f) : IsOrderIso (Function.corestrict f ⋯)

theorem TotalOrder.corestrict_strictMono_iso' {α : Type u_1} {β : Type u_2} [TotalOrder α] [PartialOrder β] {f : α → β} {s : Set β} (h : StrictMonotone f) (h' : f '' Set.univ = s) : IsOrderIso (Function.corestrict f ⋯)

theorem isLUB_iff_ub_exists_lt {α : Type u_1} {x : α} [TotalOrder α] {s : Set α} : IsLUB s x ↔ UpperBound s x ∧ ∀ (y : α), y < x → ∃ (z : α), z ∈ s ∧ y < z

theorem isGLB_iff_lb_exists_gt {α : Type u_1} {x : α} [TotalOrder α] {s : Set α} : IsGLB s x ↔ LowerBound s x ∧ ∀ (y : α), x < y → ∃ (z : α), z ∈ s ∧ z < y

instance instTotalOrderAdjoinGreatest {α : Type u_1} [TotalOrder α] : TotalOrder (AdjoinGreatest α)

Equations

• instTotalOrderAdjoinGreatest = TotalOrder.mk ⋯

def TotalOrder.carry_bij {α : Type u_1} [TotalOrder α] {β : Type u_3} (f : Function.Bijection α β) : TotalOrder β

Equations

• TotalOrder.carry_bij f = TotalOrder.mk ⋯

def IsOrderIso.totalOrder {α : Type u_1} {β : Type u_3} [TotalOrder α] [Preorder β] {f : α → β} (h : IsOrderIso f) : TotalOrder β

Equations

• h.totalOrder = TotalOrder.mk ⋯