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 α] : Prop

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.

theorem NoBotOrder.exists_not_ge {α : Type u_3} [LE α] [self : NoBotOrder α] (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 α] : Prop

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.

theorem NoTopOrder.exists_not_le {α : Type u_3} [LE α] [self : NoTopOrder α] (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 α] : Prop

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.

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

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

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

Order without maximal elements. Sometimes called cofinal.

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

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

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

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

instance nonempty_lt {α : Type u_1} [LT α] [NoMinOrder α] (a : α) : Nonempty { x : α // x < a }

Equations

• ⋯ = ⋯

instance nonempty_gt {α : Type u_1} [LT α] [NoMaxOrder α] (a : α) : Nonempty { x : α // a < x }

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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 : α) => x1 > x2) a

def IsBot {α : Type u_1} [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 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

• IsBot a = ∀ (b : α), a ≤ b

def IsTop {α : Type u_1} [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 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

• IsTop a = ∀ (b : α), b ≤ a

def IsMin {α : Type u_1} [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, isMin_iff_forall_not_lt does the conversion.

Equations

• IsMin a = ∀ ⦃b : α⦄, b ≤ a → a ≤ b

def IsMax {α : Type u_1} [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, isMax_iff_forall_not_lt does the conversion.

Equations

• IsMax a = ∀ ⦃b : α⦄, a ≤ b → b ≤ a

@[simp]

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

@[simp]

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

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

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

@[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)

Alias of the reverse direction of isTop_toDual_iff.

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)

Alias of the reverse direction of isMax_toDual_iff.

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)

Alias of the reverse direction of isTop_ofDual_iff.

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)

Alias of the reverse direction of isMax_ofDual_iff.

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

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

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

theorem IsMax.mono {α : Type u_1} [Preorder α] {a : α} {b : α} (ha : IsMax a) (h : a ≤ b) : IsMax 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

@[simp]

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

@[simp]

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

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

Alias of not_isMin_of_lt.

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

Alias of not_isMax_of_lt.

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 : α) : ¬IsMin a

@[simp]

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

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

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

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

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

theorem IsMin.eq_of_le {α : Type u_1} [PartialOrder α] {a : α} {b : α} (ha : IsMin a) (h : b ≤ a) : 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 IsMax.eq_of_ge {α : Type u_1} [PartialOrder α] {a : α} {b : α} (ha : IsMax a) (h : a ≤ b) : b = a

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 : b ≠ a) : b < a

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

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

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

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

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

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

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

theorem IsMax.prod_mk {α : 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) : IsBot x.1

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

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

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

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

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

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

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

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