Documentation

Mathlib.Order.Max

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_iff' (α : Type u_3) [LE α] :

NoBotOrder α ↔ ∀ (a : α), ∃ (b : α), ¬a ≤ b

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_iff' (α : Type u_3) [LE α] :

NoTopOrder α ↔ ∀ (a : α), ∃ (b : α), ¬b ≤ a

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_iff' (α : Type u_3) [LT α] :

NoMinOrder α ↔ ∀ (a : α), ∃ (b : α), b < a

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_iff' (α : Type u_3) [LT α] :

NoMaxOrder α ↔ ∀ (a : α), ∃ (b : α), a < b

instance nonempty_lt {α : Type u_1} [LT α] [NoMinOrder α] (a : α) :

Nonempty { x : α // x < a }

instance nonempty_gt {α : Type u_1} [LT α] [NoMaxOrder α] (a : α) :

Nonempty { x : α // a < x }

instance IsEmpty.toNoMinOrder {α : Type u_1} [LT α] [IsEmpty α] :

instance IsEmpty.toNoMaxOrder {α : Type u_1} [LT α] [IsEmpty α] :

instance OrderDual.noBotOrder {α : Type u_1} [LE α] [NoTopOrder α] :

NoBotOrder αᵒᵈ

instance OrderDual.noTopOrder {α : Type u_1} [LE α] [NoBotOrder α] :

NoTopOrder αᵒᵈ

instance OrderDual.noMinOrder {α : Type u_1} [LT α] [NoMaxOrder α] :

NoMinOrder αᵒᵈ

instance OrderDual.noMaxOrder {α : Type u_1} [LT α] [NoMinOrder α] :

NoMaxOrder αᵒᵈ

@[instance 100]

instance instNoBotOrderOfNoMinOrder {α : Type u_1} [Preorder α] [NoMinOrder α] :

@[instance 100]

instance instNoTopOrderOfNoMaxOrder {α : Type u_1} [Preorder α] [NoMaxOrder α] :

instance noMinOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder α] :

NoMinOrder (α × β)

instance noMaxOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder α] :

NoMaxOrder (α × β)

instance noMinOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder β] :

NoMinOrder (α × β)

instance noMaxOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder β] :

NoMaxOrder (α × β)

instance instNoMinOrderForallOfNonempty {ι : Type u} {π : ι → Type u_3} [Nonempty ι] [(i : ι) → Preorder (π i)] [∀ (i : ι), NoMinOrder (π i)] :

NoMinOrder ((i : ι) → π i)

instance instNoMaxOrderForallOfNonempty {ι : Type u} {π : ι → Type u_3} [Nonempty ι] [(i : ι) → Preorder (π i)] [∀ (i : ι), NoMaxOrder (π i)] :

NoMaxOrder ((i : ι) → π i)

theorem NoBotOrder.to_noMinOrder (α : Type u_3) [LinearOrder α] [NoBotOrder α] :

theorem NoTopOrder.to_noMaxOrder (α : Type u_3) [LinearOrder α] [NoTopOrder α] :

theorem noBotOrder_iff_noMinOrder (α : Type u_3) [LinearOrder α] :

NoBotOrder α ↔ NoMinOrder α

theorem noTopOrder_iff_noMaxOrder (α : Type u_3) [LinearOrder α] :

NoTopOrder α ↔ NoMaxOrder α

theorem NoMinOrder.not_acc {α : Type u_1} [LT α] [NoMinOrder α] (a : α) :

¬Acc (fun (x1 x2 : α) => x1 < x2) a

theorem NoMaxOrder.not_acc {α : Type u_1} [LT α] [NoMaxOrder α] (a : α) :

¬Acc (fun (x1 x2 : α) => x2 < x1) 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.

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.

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.

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.

Instances For

theorem noBotOrder_iff {α : Type u_1} [LE α] :

NoBotOrder α ↔ ∀ (x : α), ¬IsBot x

theorem noTopOrder_iff {α : Type u_1} [LE α] :

NoTopOrder α ↔ ∀ (x : α), ¬IsTop x

@[simp]

theorem not_isBot {α : Type u_1} [LE α] [NoBotOrder α] (a : α) :

@[simp]

theorem not_isTop {α : Type u_1} [LE α] [NoTopOrder α] (a : α) :

theorem IsBot.isMin {α : Type u_1} [LE α] {a : α} (h : IsBot a) :

theorem IsTop.isMax {α : Type u_1} [LE α] {a : α} (h : IsTop a) :

theorem IsBot.isMin_iff {α : Type u_3} [PartialOrder α] {i j : α} (h : IsBot i) :

IsMin j ↔ j = i

theorem IsTop.isMax_iff {α : Type u_3} [PartialOrder α] {i j : α} (h : IsTop i) :

IsMax j ↔ j = i

@[simp]

theorem isBot_toDual_iff {α : Type u_1} [LE α] {a : α} :

IsBot (OrderDual.toDual a) ↔ IsTop a

@[simp]

theorem isTop_toDual_iff {α : Type u_1} [LE α] {a : α} :

IsTop (OrderDual.toDual a) ↔ IsBot a

@[simp]

theorem isMin_toDual_iff {α : Type u_1} [LE α] {a : α} :

IsMin (OrderDual.toDual a) ↔ IsMax a

@[simp]

theorem isMax_toDual_iff {α : Type u_1} [LE α] {a : α} :

IsMax (OrderDual.toDual a) ↔ IsMin a

@[simp]

theorem isBot_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :

IsBot (OrderDual.ofDual a) ↔ IsTop a

@[simp]

theorem isTop_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :

IsTop (OrderDual.ofDual a) ↔ IsBot a

@[simp]

theorem isMin_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :

IsMin (OrderDual.ofDual a) ↔ IsMax a

@[simp]

theorem isMax_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :

IsMax (OrderDual.ofDual a) ↔ IsMin a

theorem IsTop.toDual {α : Type u_1} [LE α] {a : α} :

IsTop a → IsBot (OrderDual.toDual a)

Alias of the reverse direction of isBot_toDual_iff.

theorem IsBot.toDual {α : Type u_1} [LE α] {a : α} :

IsBot a → IsTop (OrderDual.toDual a)

theorem IsMax.toDual {α : Type u_1} [LE α] {a : α} :

IsMax a → IsMin (OrderDual.toDual a)

Alias of the reverse direction of isMin_toDual_iff.

theorem IsMin.toDual {α : Type u_1} [LE α] {a : α} :

IsMin a → IsMax (OrderDual.toDual a)

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

IsTop a → IsBot (OrderDual.ofDual a)

Alias of the reverse direction of isBot_ofDual_iff.

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

IsBot a → IsTop (OrderDual.ofDual a)

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

IsMax a → IsMin (OrderDual.ofDual a)

Alias of the reverse direction of isMin_ofDual_iff.

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

IsMin a → IsMax (OrderDual.ofDual a)

theorem noMinOrder_iff {α : Type u_1} [Preorder α] :

NoMinOrder α ↔ ∀ (x : α), ¬IsMin x

theorem noMaxOrder_iff {α : Type u_1} [Preorder α] :

NoMaxOrder α ↔ ∀ (x : α), ¬IsMax x

theorem IsBot.mono {α : Type u_1} [Preorder α] {a b : α} (ha : IsBot a) (h : b ≤ a) :

theorem IsTop.mono {α : Type u_1} [Preorder α] {a b : α} (ha : IsTop a) (h : a ≤ b) :

theorem IsMin.mono {α : Type u_1} [Preorder α] {a b : α} (ha : IsMin a) (h : b ≤ a) :

theorem IsMax.mono {α : Type u_1} [Preorder α] {a b : α} (ha : IsMax a) (h : a ≤ b) :

theorem IsMin.not_lt {α : Type u_1} [Preorder α] {a b : α} (h : IsMin a) :

¬b < a

theorem IsMax.not_lt {α : Type u_1} [Preorder α] {a b : α} (h : IsMax a) :

¬a < b

theorem not_isMin_of_lt {α : Type u_1} [Preorder α] {a b : α} (h : b < a) :

theorem not_isMax_of_lt {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :

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

Alias of not_isMin_of_lt.

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

theorem isMin_iff_forall_not_lt {α : Type u_1} [Preorder α] {a : α} :

IsMin a ↔ ∀ (b : α), ¬b < a

theorem isMax_iff_forall_not_lt {α : Type u_1} [Preorder α] {a : α} :

IsMax a ↔ ∀ (b : α), ¬a < b

@[simp]

theorem not_isMin_iff {α : Type u_1} [Preorder α] {a : α} :

¬IsMin a ↔ ∃ (b : α), b < a

@[simp]

theorem not_isMax_iff {α : Type u_1} [Preorder α] {a : α} :

¬IsMax a ↔ ∃ (b : α), a < b

@[simp]

theorem not_isMin {α : Type u_1} [Preorder α] [NoMinOrder α] (a : α) :

@[simp]

theorem not_isMax {α : Type u_1} [Preorder α] [NoMaxOrder α] (a : α) :

theorem Subsingleton.isBot {α : Type u_1} [Preorder α] [Subsingleton α] (a : α) :

theorem Subsingleton.isTop {α : Type u_1} [Preorder α] [Subsingleton α] (a : α) :

theorem Subsingleton.isMin {α : Type u_1} [Preorder α] [Subsingleton α] (a : α) :

theorem Subsingleton.isMax {α : Type u_1} [Preorder α] [Subsingleton α] (a : α) :

theorem IsMin.eq_of_le {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsMin a) (h : b ≤ a) :

b = a

theorem IsMax.eq_of_ge {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsMax a) (h : a ≤ b) :

b = a

theorem IsMin.eq_of_ge {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsMin a) (h : b ≤ a) :

a = b

theorem IsMax.eq_of_le {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsMax a) (h : a ≤ b) :

a = b

theorem IsBot.lt_of_ne {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsBot a) (h : a ≠ b) :

a < b

theorem IsTop.lt_of_ne' {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsTop a) (h : a ≠ b) :

b < a

theorem IsTop.lt_of_ne {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsTop a) (h : b ≠ a) :

b < a

theorem IsBot.lt_of_ne' {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsBot a) (h : b ≠ a) :

a < b

theorem IsBot.not_isMax {α : Type u_1} [PartialOrder α] {a : α} [Nontrivial α] (ha : IsBot a) :

theorem IsTop.not_isMin {α : Type u_1} [PartialOrder α] {a : α} [Nontrivial α] (ha : IsTop a) :

theorem IsBot.not_isTop {α : Type u_1} [PartialOrder α] {a : α} [Nontrivial α] (ha : IsBot a) :

theorem IsTop.not_isBot {α : Type u_1} [PartialOrder α] {a : α} [Nontrivial α] (ha : IsTop a) :

theorem IsBot.prodMk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : β} (ha : IsBot a) (hb : IsBot b) :

IsBot (a, b)

theorem IsTop.prodMk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : β} (ha : IsTop a) (hb : IsTop b) :

IsTop (a, b)

theorem IsMin.prodMk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : β} (ha : IsMin a) (hb : IsMin b) :

IsMin (a, b)

theorem IsMax.prodMk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : β} (ha : IsMax a) (hb : IsMax b) :

IsMax (a, b)

theorem IsBot.fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsBot x) :

theorem IsTop.fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsTop x) :

theorem IsBot.snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsBot x) :

theorem IsTop.snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsTop x) :

theorem IsMin.fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsMin x) :

theorem IsMax.fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsMax x) :

theorem IsMin.snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsMin x) :

theorem IsMax.snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsMax x) :

theorem Prod.isBot_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} :

IsBot x ↔ IsBot x.1 ∧ IsBot x.2

theorem Prod.isTop_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} :

IsTop x ↔ IsTop x.1 ∧ IsTop x.2

theorem Prod.isMin_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} :

IsMin x ↔ IsMin x.1 ∧ IsMin x.2

theorem Prod.isMax_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} :

IsMax x ↔ IsMax x.1 ∧ IsMax x.2