# Minimal/maximal and bottom/top elements #

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

## Predicates #

• IsBot: An element is bottom if all elements are greater than it.
• IsTop: An element is top if all elements are less than it.
• IsMin: An element is minimal if no element is strictly less than it.
• IsMax: An element is maximal if no element is strictly greater than it.

See also isBot_iff_isMin and isTop_iff_isMax for the equivalences in a (co)directed order.

## Typeclasses #

• NoBotOrder: An order without bottom elements.
• NoTopOrder: An order without top elements.
• NoMinOrder: An order without minimal elements.
• NoMaxOrder: An order without maximal elements.
class NoBotOrder (α : Type u_3) [LE α] :

Order without bottom elements.

• exists_not_ge : ∀ (a : α), ∃ (b : α), ¬a b

For each term a, there is some b which is either incomparable or strictly smaller.

Instances
theorem NoBotOrder.exists_not_ge {α : Type u_3} [LE α] [self : ] (a : α) :
∃ (b : α), ¬a b

For each term a, there is some b which is either incomparable or strictly smaller.

class NoTopOrder (α : Type u_3) [LE α] :

Order without top elements.

• exists_not_le : ∀ (a : α), ∃ (b : α), ¬b a

For each term a, there is some b which is either incomparable or strictly larger.

Instances
theorem NoTopOrder.exists_not_le {α : Type u_3} [LE α] [self : ] (a : α) :
∃ (b : α), ¬b a

For each term a, there is some b which is either incomparable or strictly larger.

class NoMinOrder (α : Type u_3) [LT α] :

Order without minimal elements. Sometimes called coinitial or dense.

• exists_lt : ∀ (a : α), ∃ (b : α), b < a

For each term a, there is some strictly smaller b.

Instances
theorem NoMinOrder.exists_lt {α : Type u_3} [LT α] [self : ] (a : α) :
∃ (b : α), b < a

For each term a, there is some strictly smaller b.

class NoMaxOrder (α : Type u_3) [LT α] :

Order without maximal elements. Sometimes called cofinal.

• exists_gt : ∀ (a : α), ∃ (b : α), a < b

For each term a, there is some strictly greater b.

Instances
theorem NoMaxOrder.exists_gt {α : Type u_3} [LT α] [self : ] (a : α) :
∃ (b : α), a < b

For each term a, there is some strictly greater b.

instance nonempty_lt {α : Type u_1} [LT α] [] (a : α) :
Nonempty { x : α // x < a }
Equations
• =
instance nonempty_gt {α : Type u_1} [LT α] [] (a : α) :
Nonempty { x : α // a < x }
Equations
• =
instance IsEmpty.toNoMaxOrder {α : Type u_1} [LT α] [] :
Equations
• =
instance IsEmpty.toNoMinOrder {α : Type u_1} [LT α] [] :
Equations
• =
instance OrderDual.noBotOrder {α : Type u_1} [LE α] [] :
Equations
• =
instance OrderDual.noTopOrder {α : Type u_1} [LE α] [] :
Equations
• =
instance OrderDual.noMinOrder {α : Type u_1} [LT α] [] :
Equations
• =
instance OrderDual.noMaxOrder {α : Type u_1} [LT α] [] :
Equations
• =
@[instance 100]
instance instNoBotOrderOfNoMinOrder {α : Type u_1} [] [] :
Equations
• =
@[instance 100]
instance instNoTopOrderOfNoMaxOrder {α : Type u_1} [] [] :
Equations
• =
instance noMaxOrder_of_left {α : Type u_1} {β : Type u_2} [] [] [] :
NoMaxOrder (α × β)
Equations
• =
instance noMaxOrder_of_right {α : Type u_1} {β : Type u_2} [] [] [] :
NoMaxOrder (α × β)
Equations
• =
instance noMinOrder_of_left {α : Type u_1} {β : Type u_2} [] [] [] :
NoMinOrder (α × β)
Equations
• =
instance noMinOrder_of_right {α : Type u_1} {β : Type u_2} [] [] [] :
NoMinOrder (α × β)
Equations
• =
instance instNoMaxOrderForallOfNonempty {ι : Type u} {π : ιType u_3} [] [(i : ι) → Preorder (π i)] [∀ (i : ι), NoMaxOrder (π i)] :
NoMaxOrder ((i : ι) → π i)
Equations
• =
instance instNoMinOrderForallOfNonempty {ι : Type u} {π : ιType u_3} [] [(i : ι) → Preorder (π i)] [∀ (i : ι), NoMinOrder (π i)] :
NoMinOrder ((i : ι) → π i)
Equations
• =
theorem NoBotOrder.to_noMinOrder (α : Type u_3) [] [] :
theorem NoTopOrder.to_noMaxOrder (α : Type u_3) [] [] :
theorem noBotOrder_iff_noMinOrder (α : Type u_3) [] :
theorem noTopOrder_iff_noMaxOrder (α : Type u_3) [] :
theorem NoMinOrder.not_acc {α : Type u_1} [LT α] [] (a : α) :
¬Acc (fun (x x_1 : α) => x < x_1) a
theorem NoMaxOrder.not_acc {α : Type u_1} [LT α] [] (a : α) :
¬Acc (fun (x x_1 : α) => x > x_1) a
def IsBot {α : Type u_1} [LE α] (a : α) :

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 OrderBot, except that a preorder may have several bottom elements. When α is linear, this is useful to make a case disjunction on NoMinOrder α within a proof.

Equations
• = ∀ (b : α), a b
Instances For
def IsTop {α : Type u_1} [LE α] (a : α) :

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 OrderBot, except that a preorder may have several top elements. When α is linear, this is useful to make a case disjunction on NoMaxOrder α within a proof.

Equations
• = ∀ (b : α), b a
Instances For
def IsMin {α : Type u_1} [LE α] (a : α) :

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, isMin_iff_forall_not_lt does the conversion.

Equations
• = ∀ ⦃b : α⦄, b aa b
Instances For
def IsMax {α : Type u_1} [LE α] (a : α) :

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, isMax_iff_forall_not_lt does the conversion.

Equations
• = ∀ ⦃b : α⦄, a bb a
Instances For
@[simp]
theorem not_isBot {α : Type u_1} [LE α] [] (a : α) :
@[simp]
theorem not_isTop {α : Type u_1} [LE α] [] (a : α) :
theorem IsBot.isMin {α : Type u_1} [LE α] {a : α} (h : ) :
theorem IsTop.isMax {α : Type u_1} [LE α] {a : α} (h : ) :
@[simp]
theorem isBot_toDual_iff {α : Type u_1} [LE α] {a : α} :
IsBot (OrderDual.toDual a)
@[simp]
theorem isTop_toDual_iff {α : Type u_1} [LE α] {a : α} :
IsTop (OrderDual.toDual a)
@[simp]
theorem isMin_toDual_iff {α : Type u_1} [LE α] {a : α} :
IsMin (OrderDual.toDual a)
@[simp]
theorem isMax_toDual_iff {α : Type u_1} [LE α] {a : α} :
IsMax (OrderDual.toDual a)
@[simp]
theorem isBot_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
IsBot (OrderDual.ofDual a)
@[simp]
theorem isTop_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
IsTop (OrderDual.ofDual a)
@[simp]
theorem isMin_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
IsMin (OrderDual.ofDual a)
@[simp]
theorem isMax_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
IsMax (OrderDual.ofDual a)
theorem IsTop.toDual {α : Type u_1} [LE α] {a : α} :
IsBot (OrderDual.toDual a)

Alias of the reverse direction of isBot_toDual_iff.

theorem IsBot.toDual {α : Type u_1} [LE α] {a : α} :
IsTop (OrderDual.toDual a)

Alias of the reverse direction of isTop_toDual_iff.

theorem IsMax.toDual {α : Type u_1} [LE α] {a : α} :
IsMin (OrderDual.toDual a)

Alias of the reverse direction of isMin_toDual_iff.

theorem IsMin.toDual {α : Type u_1} [LE α] {a : α} :
IsMax (OrderDual.toDual a)

Alias of the reverse direction of isMax_toDual_iff.

theorem IsTop.ofDual {α : Type u_1} [LE α] {a : αᵒᵈ} :
IsBot (OrderDual.ofDual a)

Alias of the reverse direction of isBot_ofDual_iff.

theorem IsBot.ofDual {α : Type u_1} [LE α] {a : αᵒᵈ} :
IsTop (OrderDual.ofDual a)

Alias of the reverse direction of isTop_ofDual_iff.

theorem IsMax.ofDual {α : Type u_1} [LE α] {a : αᵒᵈ} :
IsMin (OrderDual.ofDual a)

Alias of the reverse direction of isMin_ofDual_iff.

theorem IsMin.ofDual {α : Type u_1} [LE α] {a : αᵒᵈ} :
IsMax (OrderDual.ofDual a)

Alias of the reverse direction of isMax_ofDual_iff.

theorem IsBot.mono {α : Type u_1} [] {a : α} {b : α} (ha : ) (h : b a) :
theorem IsTop.mono {α : Type u_1} [] {a : α} {b : α} (ha : ) (h : a b) :
theorem IsMin.mono {α : Type u_1} [] {a : α} {b : α} (ha : ) (h : b a) :
theorem IsMax.mono {α : Type u_1} [] {a : α} {b : α} (ha : ) (h : a b) :
theorem IsMin.not_lt {α : Type u_1} [] {a : α} {b : α} (h : ) :
¬b < a
theorem IsMax.not_lt {α : Type u_1} [] {a : α} {b : α} (h : ) :
¬a < b
@[simp]
theorem not_isMin_of_lt {α : Type u_1} [] {a : α} {b : α} (h : b < a) :
@[simp]
theorem not_isMax_of_lt {α : Type u_1} [] {a : α} {b : α} (h : a < b) :
theorem LT.lt.not_isMin {α : Type u_1} [] {a : α} {b : α} (h : b < a) :

Alias of not_isMin_of_lt.

theorem LT.lt.not_isMax {α : Type u_1} [] {a : α} {b : α} (h : a < b) :

Alias of not_isMax_of_lt.

theorem isMin_iff_forall_not_lt {α : Type u_1} [] {a : α} :
∀ (b : α), ¬b < a
theorem isMax_iff_forall_not_lt {α : Type u_1} [] {a : α} :
∀ (b : α), ¬a < b
@[simp]
theorem not_isMin_iff {α : Type u_1} [] {a : α} :
¬ ∃ (b : α), b < a
@[simp]
theorem not_isMax_iff {α : Type u_1} [] {a : α} :
¬ ∃ (b : α), a < b
@[simp]
theorem not_isMin {α : Type u_1} [] [] (a : α) :
@[simp]
theorem not_isMax {α : Type u_1} [] [] (a : α) :
theorem Subsingleton.isBot {α : Type u_1} [] [] (a : α) :
theorem Subsingleton.isTop {α : Type u_1} [] [] (a : α) :
theorem Subsingleton.isMin {α : Type u_1} [] [] (a : α) :
theorem Subsingleton.isMax {α : Type u_1} [] [] (a : α) :
theorem IsMin.eq_of_le {α : Type u_1} [] {a : α} {b : α} (ha : ) (h : b a) :
b = a
theorem IsMin.eq_of_ge {α : Type u_1} [] {a : α} {b : α} (ha : ) (h : b a) :
a = b
theorem IsMax.eq_of_le {α : Type u_1} [] {a : α} {b : α} (ha : ) (h : a b) :
a = b
theorem IsMax.eq_of_ge {α : Type u_1} [] {a : α} {b : α} (ha : ) (h : a b) :
b = a
theorem IsBot.prod_mk {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : β} (ha : ) (hb : ) :
IsBot (a, b)
theorem IsTop.prod_mk {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : β} (ha : ) (hb : ) :
IsTop (a, b)
theorem IsMin.prod_mk {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : β} (ha : ) (hb : ) :
IsMin (a, b)
theorem IsMax.prod_mk {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : β} (ha : ) (hb : ) :
IsMax (a, b)
theorem IsBot.fst {α : Type u_1} {β : Type u_2} [] [] {x : α × β} (hx : ) :
IsBot x.1
theorem IsBot.snd {α : Type u_1} {β : Type u_2} [] [] {x : α × β} (hx : ) :
IsBot x.2
theorem IsTop.fst {α : Type u_1} {β : Type u_2} [] [] {x : α × β} (hx : ) :
IsTop x.1
theorem IsTop.snd {α : Type u_1} {β : Type u_2} [] [] {x : α × β} (hx : ) :
IsTop x.2
theorem IsMin.fst {α : Type u_1} {β : Type u_2} [] [] {x : α × β} (hx : ) :
IsMin x.1
theorem IsMin.snd {α : Type u_1} {β : Type u_2} [] [] {x : α × β} (hx : ) :
IsMin x.2
theorem IsMax.fst {α : Type u_1} {β : Type u_2} [] [] {x : α × β} (hx : ) :
IsMax x.1
theorem IsMax.snd {α : Type u_1} {β : Type u_2} [] [] {x : α × β} (hx : ) :
IsMax x.2
theorem Prod.isBot_iff {α : Type u_1} {β : Type u_2} [] [] {x : α × β} :
IsBot x.1 IsBot x.2
theorem Prod.isTop_iff {α : Type u_1} {β : Type u_2} [] [] {x : α × β} :
IsTop x.1 IsTop x.2
theorem Prod.isMin_iff {α : Type u_1} {β : Type u_2} [] [] {x : α × β} :
IsMin x.1 IsMin x.2
theorem Prod.isMax_iff {α : Type u_1} {β : Type u_2} [] [] {x : α × β} :
IsMax x.1 IsMax x.2