order.max

# Minimal/maximal and bottom/top elements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines predicates for elements to be minimal/maximal or bottom/top and typeclasses saying that there are no such elements.

## Predicates #

• is_bot: An element is bottom if all elements are greater than it.
• is_top: An element is top if all elements are less than it.
• is_min: An element is minimal if no element is strictly less than it.
• is_max: An element is maximal if no element is strictly greater than it.

See also is_bot_iff_is_min and is_top_iff_is_max for the equivalences in a (co)directed order.

## Typeclasses #

• no_bot_order: An order without bottom elements.
• no_top_order: An order without top elements.
• no_min_order: An order without minimal elements.
• no_max_order: An order without maximal elements.
@[class]
structure no_bot_order (α : Type u_5) [has_le α] :
Prop

Order without bottom elements.

Instances of this typeclass
@[class]
structure no_top_order (α : Type u_5) [has_le α] :
Prop

Order without top elements.

Instances of this typeclass
@[class]
structure no_min_order (α : Type u_5) [has_lt α] :
Prop
• exists_lt : (a : α), (b : α), b < a

Order without minimal elements. Sometimes called coinitial or dense.

Instances of this typeclass
@[class]
structure no_max_order (α : Type u_5) [has_lt α] :
Prop
• exists_gt : (a : α), (b : α), a < b

Order without maximal elements. Sometimes called cofinal.

Instances of this typeclass
@[protected, instance]
def nonempty_lt {α : Type u_2} [has_lt α] [no_min_order α] (a : α) :
nonempty {x // x < a}
@[protected, instance]
def nonempty_gt {α : Type u_2} [has_lt α] [no_max_order α] (a : α) :
nonempty {x // a < x}
@[protected, instance]
def order_dual.no_bot_order (α : Type u_1) [has_le α] [no_top_order α] :
@[protected, instance]
def order_dual.no_top_order (α : Type u_1) [has_le α] [no_bot_order α] :
@[protected, instance]
def order_dual.no_min_order (α : Type u_1) [has_lt α] [no_max_order α] :
@[protected, instance]
def order_dual.no_max_order (α : Type u_1) [has_lt α] [no_min_order α] :
@[protected, instance]
def no_max_order_of_left {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [no_max_order α] :
@[protected, instance]
def no_max_order_of_right {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [no_max_order β] :
@[protected, instance]
def no_min_order_of_left {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [no_min_order α] :
@[protected, instance]
def no_min_order_of_right {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [no_min_order β] :
@[protected, instance]
def pi.no_max_order {ι : Type u_1} {π : ι Type u_4} [nonempty ι] [Π (i : ι), preorder (π i)] [ (i : ι), no_max_order (π i)] :
no_max_order (Π (i : ι), π i)
@[protected, instance]
def pi.no_min_order {ι : Type u_1} {π : ι Type u_4} [nonempty ι] [Π (i : ι), preorder (π i)] [ (i : ι), no_min_order (π i)] :
no_min_order (Π (i : ι), π i)
@[protected, instance]
@[protected, instance]
theorem no_min_order.not_acc {α : Type u_2} [has_lt α] [no_min_order α] (a : α) :
theorem no_max_order.not_acc {α : Type u_2} [has_lt α] [no_max_order α] (a : α) :
¬ a
def is_bot {α : Type u_2} [has_le α] (a : α) :
Prop

a : α is a bottom element of α if it is less than or equal to any other element of α. This predicate is roughly an unbundled version of order_bot, except that a preorder may have several bottom elements. When α is linear, this is useful to make a case disjunction on no_min_order α within a proof.

Equations
def is_top {α : Type u_2} [has_le α] (a : α) :
Prop

a : α is a top element of α if it is greater than or equal to any other element of α. This predicate is roughly an unbundled version of order_bot, except that a preorder may have several top elements. When α is linear, this is useful to make a case disjunction on no_max_order α within a proof.

Equations
def is_min {α : Type u_2} [has_le α] (a : α) :
Prop

a is a minimal element of α if no element is strictly less than it. We spell it without < to avoid having to convert between ≤ and <. Instead, is_min_iff_forall_not_lt does the conversion.

Equations
def is_max {α : Type u_2} [has_le α] (a : α) :
Prop

a is a maximal element of α if no element is strictly greater than it. We spell it without < to avoid having to convert between ≤ and <. Instead, is_max_iff_forall_not_lt does the conversion.

Equations
@[simp]
theorem not_is_bot {α : Type u_2} [has_le α] [no_bot_order α] (a : α) :
@[simp]
theorem not_is_top {α : Type u_2} [has_le α] [no_top_order α] (a : α) :
@[protected]
theorem is_bot.is_min {α : Type u_2} [has_le α] {a : α} (h : is_bot a) :
@[protected]
theorem is_top.is_max {α : Type u_2} [has_le α] {a : α} (h : is_top a) :
@[simp]
theorem is_bot_to_dual_iff {α : Type u_2} [has_le α] {a : α} :
@[simp]
theorem is_top_to_dual_iff {α : Type u_2} [has_le α] {a : α} :
@[simp]
theorem is_min_to_dual_iff {α : Type u_2} [has_le α] {a : α} :
@[simp]
theorem is_max_to_dual_iff {α : Type u_2} [has_le α] {a : α} :
@[simp]
theorem is_bot_of_dual_iff {α : Type u_2} [has_le α] {a : αᵒᵈ} :
@[simp]
theorem is_top_of_dual_iff {α : Type u_2} [has_le α] {a : αᵒᵈ} :
@[simp]
theorem is_min_of_dual_iff {α : Type u_2} [has_le α] {a : αᵒᵈ} :
@[simp]
theorem is_max_of_dual_iff {α : Type u_2} [has_le α] {a : αᵒᵈ} :
theorem is_top.to_dual {α : Type u_2} [has_le α] {a : α} :

Alias of the reverse direction of is_bot_to_dual_iff.

theorem is_bot.to_dual {α : Type u_2} [has_le α] {a : α} :

Alias of the reverse direction of is_top_to_dual_iff.

theorem is_max.to_dual {α : Type u_2} [has_le α] {a : α} :

Alias of the reverse direction of is_min_to_dual_iff.

theorem is_min.to_dual {α : Type u_2} [has_le α] {a : α} :

Alias of the reverse direction of is_max_to_dual_iff.

theorem is_top.of_dual {α : Type u_2} [has_le α] {a : αᵒᵈ} :

Alias of the reverse direction of is_bot_of_dual_iff.

theorem is_bot.of_dual {α : Type u_2} [has_le α] {a : αᵒᵈ} :

Alias of the reverse direction of is_top_of_dual_iff.

theorem is_max.of_dual {α : Type u_2} [has_le α] {a : αᵒᵈ} :

Alias of the reverse direction of is_min_of_dual_iff.

theorem is_min.of_dual {α : Type u_2} [has_le α] {a : αᵒᵈ} :

Alias of the reverse direction of is_max_of_dual_iff.

theorem is_bot.mono {α : Type u_2} [preorder α] {a b : α} (ha : is_bot a) (h : b a) :
theorem is_top.mono {α : Type u_2} [preorder α] {a b : α} (ha : is_top a) (h : a b) :
theorem is_min.mono {α : Type u_2} [preorder α] {a b : α} (ha : is_min a) (h : b a) :
theorem is_max.mono {α : Type u_2} [preorder α] {a b : α} (ha : is_max a) (h : a b) :
theorem is_min.not_lt {α : Type u_2} [preorder α] {a b : α} (h : is_min a) :
¬b < a
theorem is_max.not_lt {α : Type u_2} [preorder α] {a b : α} (h : is_max a) :
¬a < b
@[simp]
theorem not_is_min_of_lt {α : Type u_2} [preorder α] {a b : α} (h : b < a) :
@[simp]
theorem not_is_max_of_lt {α : Type u_2} [preorder α] {a b : α} (h : a < b) :
theorem has_lt.lt.not_is_min {α : Type u_2} [preorder α] {a b : α} (h : b < a) :

Alias of not_is_min_of_lt.

theorem has_lt.lt.not_is_max {α : Type u_2} [preorder α] {a b : α} (h : a < b) :

Alias of not_is_max_of_lt.

theorem is_min_iff_forall_not_lt {α : Type u_2} [preorder α] {a : α} :
(b : α), ¬b < a
theorem is_max_iff_forall_not_lt {α : Type u_2} [preorder α] {a : α} :
(b : α), ¬a < b
@[simp]
theorem not_is_min_iff {α : Type u_2} [preorder α] {a : α} :
¬ (b : α), b < a
@[simp]
theorem not_is_max_iff {α : Type u_2} [preorder α] {a : α} :
¬ (b : α), a < b
@[simp]
theorem not_is_min {α : Type u_2} [preorder α] [no_min_order α] (a : α) :
@[simp]
theorem not_is_max {α : Type u_2} [preorder α] [no_max_order α] (a : α) :
@[protected]
theorem subsingleton.is_bot {α : Type u_2} [preorder α] [subsingleton α] (a : α) :
@[protected]
theorem subsingleton.is_top {α : Type u_2} [preorder α] [subsingleton α] (a : α) :
@[protected]
theorem subsingleton.is_min {α : Type u_2} [preorder α] [subsingleton α] (a : α) :
@[protected]
theorem subsingleton.is_max {α : Type u_2} [preorder α] [subsingleton α] (a : α) :
@[protected]
theorem is_min.eq_of_le {α : Type u_2} {a b : α} (ha : is_min a) (h : b a) :
b = a
@[protected]
theorem is_min.eq_of_ge {α : Type u_2} {a b : α} (ha : is_min a) (h : b a) :
a = b
@[protected]
theorem is_max.eq_of_le {α : Type u_2} {a b : α} (ha : is_max a) (h : a b) :
a = b
@[protected]
theorem is_max.eq_of_ge {α : Type u_2} {a b : α} (ha : is_max a) (h : a b) :
b = a
theorem is_bot.prod_mk {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {a : α} {b : β} (ha : is_bot a) (hb : is_bot b) :
is_bot (a, b)
theorem is_top.prod_mk {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {a : α} {b : β} (ha : is_top a) (hb : is_top b) :
is_top (a, b)
theorem is_min.prod_mk {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {a : α} {b : β} (ha : is_min a) (hb : is_min b) :
is_min (a, b)
theorem is_max.prod_mk {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {a : α} {b : β} (ha : is_max a) (hb : is_max b) :
is_max (a, b)
theorem is_bot.fst {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} (hx : is_bot x) :
theorem is_bot.snd {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} (hx : is_bot x) :
theorem is_top.fst {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} (hx : is_top x) :
theorem is_top.snd {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} (hx : is_top x) :
theorem is_min.fst {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} (hx : is_min x) :
theorem is_min.snd {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} (hx : is_min x) :
theorem is_max.fst {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} (hx : is_max x) :
theorem is_max.snd {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} (hx : is_max x) :
theorem prod.is_bot_iff {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} :
theorem prod.is_top_iff {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} :
theorem prod.is_min_iff {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} :
theorem prod.is_max_iff {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} :