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 #

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

Typeclasses #

source
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.

Instances
source
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.

Instances
source
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.

Instances
source
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.

Instances
source
instance nonempty_lt {α : Type u_1} [LT α] [NoMinOrder α] (a : α) :
Nonempty { x : α // x < a }
source
instance nonempty_gt {α : Type u_1} [LT α] [NoMaxOrder α] (a : α) :
Nonempty { x : α // a < x }
source
instance IsEmpty.toNoMaxOrder {α : Type u_1} [LT α] [IsEmpty α] :
NoMaxOrder α
source
instance IsEmpty.toNoMinOrder {α : Type u_1} [LT α] [IsEmpty α] :
NoMinOrder α
source
instance OrderDual.noBotOrder {α : Type u_1} [LE α] [NoTopOrder α] :
NoBotOrder αᵒᵈ
source
instance OrderDual.noTopOrder {α : Type u_1} [LE α] [NoBotOrder α] :
NoTopOrder αᵒᵈ
source
instance OrderDual.noMinOrder {α : Type u_1} [LT α] [NoMaxOrder α] :
NoMinOrder αᵒᵈ
source
instance OrderDual.noMaxOrder {α : Type u_1} [LT α] [NoMinOrder α] :
NoMaxOrder αᵒᵈ
source
@[instance 100]
instance instNoBotOrderOfNoMinOrder {α : Type u_1} [Preorder α] [NoMinOrder α] :
NoBotOrder α
source
@[instance 100]
instance instNoTopOrderOfNoMaxOrder {α : Type u_1} [Preorder α] [NoMaxOrder α] :
NoTopOrder α
source
instance noMaxOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder α] :
NoMaxOrder (α × β)
source
instance noMaxOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMaxOrder β] :
NoMaxOrder (α × β)
source
instance noMinOrder_of_left {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder α] :
NoMinOrder (α × β)
source
instance noMinOrder_of_right {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [NoMinOrder β] :
NoMinOrder (α × β)
source
instance instNoMaxOrderForallOfNonempty {ι : Type u} {π : ι → Type u_3} [Nonempty ι] [(i : ι) → Preorder (π i)] [∀ (i : ι), NoMaxOrder (π i)] :
NoMaxOrder ((i : ι) → π i)
source
instance instNoMinOrderForallOfNonempty {ι : Type u} {π : ι → Type u_3} [Nonempty ι] [(i : ι) → Preorder (π i)] [∀ (i : ι), NoMinOrder (π i)] :
NoMinOrder ((i : ι) → π i)
source
theorem NoBotOrder.to_noMinOrder (α : Type u_3) [LinearOrder α] [NoBotOrder α] :
NoMinOrder α
source
theorem NoTopOrder.to_noMaxOrder (α : Type u_3) [LinearOrder α] [NoTopOrder α] :
NoMaxOrder α
source
theorem noBotOrder_iff_noMinOrder (α : Type u_3) [LinearOrder α] :
NoBotOrder α ↔ NoMinOrder α
source
theorem noTopOrder_iff_noMaxOrder (α : Type u_3) [LinearOrder α] :
NoTopOrder α ↔ NoMaxOrder α
source
theorem NoMinOrder.not_acc {α : Type u_1} [LT α] [NoMinOrder α] (a : α) :
¬Acc (fun (x1 x2 : α) => x1 < x2) a
source
theorem NoMaxOrder.not_acc {α : Type u_1} [LT α] [NoMaxOrder α] (a : α) :
¬Acc (fun (x1 x2 : α) => x1 > x2) a
source
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
source
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
source
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
source
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
source
@[simp]
theorem not_isBot {α : Type u_1} [LE α] [NoBotOrder α] (a : α) :
¬IsBot a
source
@[simp]
theorem not_isTop {α : Type u_1} [LE α] [NoTopOrder α] (a : α) :
¬IsTop a
source
theorem IsBot.isMin {α : Type u_1} [LE α] {a : α} (h : IsBot a) :
IsMin a
source
theorem IsTop.isMax {α : Type u_1} [LE α] {a : α} (h : IsTop a) :
IsMax a
source
theorem IsTop.isMax_iff {α : Type u_3} [PartialOrder α] {i j : α} (h : IsTop i) :
IsMax j ↔ j = i
source
theorem IsBot.isMin_iff {α : Type u_3} [PartialOrder α] {i j : α} (h : IsBot i) :
IsMin j ↔ j = i
source
@[simp]
theorem isBot_toDual_iff {α : Type u_1} [LE α] {a : α} :
IsBot (OrderDual.toDual a) ↔ IsTop a
source
@[simp]
theorem isTop_toDual_iff {α : Type u_1} [LE α] {a : α} :
IsTop (OrderDual.toDual a) ↔ IsBot a
source
@[simp]
theorem isMin_toDual_iff {α : Type u_1} [LE α] {a : α} :
IsMin (OrderDual.toDual a) ↔ IsMax a
source
@[simp]
theorem isMax_toDual_iff {α : Type u_1} [LE α] {a : α} :
IsMax (OrderDual.toDual a) ↔ IsMin a
source
@[simp]
theorem isBot_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
IsBot (OrderDual.ofDual a) ↔ IsTop a
source
@[simp]
theorem isTop_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
IsTop (OrderDual.ofDual a) ↔ IsBot a
source
@[simp]
theorem isMin_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
IsMin (OrderDual.ofDual a) ↔ IsMax a
source
@[simp]
theorem isMax_ofDual_iff {α : Type u_1} [LE α] {a : αᵒᵈ} :
IsMax (OrderDual.ofDual a) ↔ IsMin a
source
theorem IsTop.toDual {α : Type u_1} [LE α] {a : α} :
IsTop a → IsBot (OrderDual.toDual a)

Alias of the reverse direction of isBot_toDual_iff.

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

Alias of the reverse direction of isTop_toDual_iff.

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

Alias of the reverse direction of isMin_toDual_iff.

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

Alias of the reverse direction of isMax_toDual_iff.

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

Alias of the reverse direction of isBot_ofDual_iff.

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

Alias of the reverse direction of isTop_ofDual_iff.

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

Alias of the reverse direction of isMin_ofDual_iff.

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

Alias of the reverse direction of isMax_ofDual_iff.

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

Alias of not_isMin_of_lt.

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

Alias of not_isMax_of_lt.

source
theorem isMin_iff_forall_not_lt {α : Type u_1} [Preorder α] {a : α} :
IsMin a ↔ ∀ (b : α), ¬b < a
source
theorem isMax_iff_forall_not_lt {α : Type u_1} [Preorder α] {a : α} :
IsMax a ↔ ∀ (b : α), ¬a < b
source
@[simp]
theorem not_isMin_iff {α : Type u_1} [Preorder α] {a : α} :
¬IsMin a ↔ ∃ (b : α), b < a
source
@[simp]
theorem not_isMax_iff {α : Type u_1} [Preorder α] {a : α} :
¬IsMax a ↔ ∃ (b : α), a < b
source
@[simp]
theorem not_isMin {α : Type u_1} [Preorder α] [NoMinOrder α] (a : α) :
¬IsMin a
source
@[simp]
theorem not_isMax {α : Type u_1} [Preorder α] [NoMaxOrder α] (a : α) :
¬IsMax a
source
theorem Subsingleton.isBot {α : Type u_1} [Preorder α] [Subsingleton α] (a : α) :
IsBot a
source
theorem Subsingleton.isTop {α : Type u_1} [Preorder α] [Subsingleton α] (a : α) :
IsTop a
source
theorem Subsingleton.isMin {α : Type u_1} [Preorder α] [Subsingleton α] (a : α) :
IsMin a
source
theorem Subsingleton.isMax {α : Type u_1} [Preorder α] [Subsingleton α] (a : α) :
IsMax a
source
theorem IsMin.eq_of_le {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsMin a) (h : b ≤ a) :
b = a
source
theorem IsMin.eq_of_ge {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsMin a) (h : b ≤ a) :
a = b
source
theorem IsMax.eq_of_le {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsMax a) (h : a ≤ b) :
a = b
source
theorem IsMax.eq_of_ge {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsMax a) (h : a ≤ b) :
b = a
source
theorem IsBot.lt_of_ne {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsBot a) (h : a ≠ b) :
a < b
source
theorem IsTop.lt_of_ne {α : Type u_1} [PartialOrder α] {a b : α} (ha : IsTop a) (h : b ≠ a) :
b < a
source
theorem IsBot.not_isMax {α : Type u_1} [PartialOrder α] {a : α} [Nontrivial α] (ha : IsBot a) :
¬IsMax a
source
theorem IsTop.not_isMin {α : Type u_1} [PartialOrder α] {a : α} [Nontrivial α] (ha : IsTop a) :
¬IsMin a
source
theorem IsBot.not_isTop {α : Type u_1} [PartialOrder α] {a : α} [Nontrivial α] (ha : IsBot a) :
¬IsTop a
source
theorem IsTop.not_isBot {α : Type u_1} [PartialOrder α] {a : α} [Nontrivial α] (ha : IsTop a) :
¬IsBot a
source
theorem IsBot.prodMk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : β} (ha : IsBot a) (hb : IsBot b) :
IsBot (a, b)
source
@[deprecated IsBot.prodMk (since := "2025-02-22")]
theorem IsBot.prod_mk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : β} (ha : IsBot a) (hb : IsBot b) :
IsBot (a, b)

Alias of IsBot.prodMk.

source
theorem IsTop.prodMk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : β} (ha : IsTop a) (hb : IsTop b) :
IsTop (a, b)
source
@[deprecated IsTop.prodMk (since := "2025-02-22")]
theorem IsTop.prod_mk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : β} (ha : IsTop a) (hb : IsTop b) :
IsTop (a, b)

Alias of IsTop.prodMk.

source
theorem IsMin.prodMk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : β} (ha : IsMin a) (hb : IsMin b) :
IsMin (a, b)
source
@[deprecated IsMin.prodMk (since := "2025-02-22")]
theorem IsMin.prod_mk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : β} (ha : IsMin a) (hb : IsMin b) :
IsMin (a, b)

Alias of IsMin.prodMk.

source
theorem IsMax.prodMk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : β} (ha : IsMax a) (hb : IsMax b) :
IsMax (a, b)
source
@[deprecated IsMax.prodMk (since := "2025-02-22")]
theorem IsMax.prod_mk {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : β} (ha : IsMax a) (hb : IsMax b) :
IsMax (a, b)

Alias of IsMax.prodMk.

source
theorem IsBot.fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsBot x) :
IsBot x.fst
source
theorem IsBot.snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsBot x) :
IsBot x.snd
source
theorem IsTop.fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsTop x) :
IsTop x.fst
source
theorem IsTop.snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsTop x) :
IsTop x.snd
source
theorem IsMin.fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsMin x) :
IsMin x.fst
source
theorem IsMin.snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsMin x) :
IsMin x.snd
source
theorem IsMax.fst {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsMax x) :
IsMax x.fst
source
theorem IsMax.snd {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} (hx : IsMax x) :
IsMax x.snd
source
theorem Prod.isBot_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} :
IsBot x ↔ IsBot x.fst ∧ IsBot x.snd
source
theorem Prod.isTop_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} :
IsTop x ↔ IsTop x.fst ∧ IsTop x.snd
source
theorem Prod.isMin_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} :
IsMin x ↔ IsMin x.fst ∧ IsMin x.snd
source
theorem Prod.isMax_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {x : α × β} :
IsMax x ↔ IsMax x.fst ∧ IsMax x.snd