mathlib3 documentation

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

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

Order without bottom elements.

Instances of this typeclass

@[class]

structure no_top_order (α : Type u_5) [has_le α] :

Prop

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

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

no_bot_order αᵒᵈ

@[protected, instance]

def order_dual.no_top_order (α : Type u_1) [has_le α] [no_bot_order α] :

no_top_order αᵒᵈ

@[protected, instance]

def order_dual.no_min_order (α : Type u_1) [has_lt α] [no_max_order α] :

no_min_order αᵒᵈ

@[protected, instance]

def order_dual.no_max_order (α : Type u_1) [has_lt α] [no_min_order α] :

no_max_order αᵒᵈ

@[protected, instance]

def no_max_order_of_left {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [no_max_order α] :

no_max_order (α × β)

@[protected, instance]

def no_max_order_of_right {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [no_max_order β] :

no_max_order (α × β)

@[protected, instance]

def no_min_order_of_left {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [no_min_order α] :

no_min_order (α × β)

@[protected, instance]

def no_min_order_of_right {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [no_min_order β] :

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]

def no_min_order.to_no_bot_order (α : Type u_1) [preorder α] [no_min_order α] :

no_bot_order α

@[protected, instance]

def no_max_order.to_no_top_order (α : Type u_1) [preorder α] [no_max_order α] :

no_top_order α

theorem no_bot_order.to_no_min_order (α : Type u_1) [linear_order α] [no_bot_order α] :

no_min_order α

theorem no_top_order.to_no_max_order (α : Type u_1) [linear_order α] [no_top_order α] :

no_max_order α

theorem no_bot_order_iff_no_min_order (α : Type u_1) [linear_order α] :

no_bot_order α ↔ no_min_order α

theorem no_top_order_iff_no_max_order (α : Type u_1) [linear_order α] :

no_top_order α ↔ no_max_order α

theorem no_min_order.not_acc {α : Type u_2} [has_lt α] [no_min_order α] (a : α) :

¬acc has_lt.lt a

theorem no_max_order.not_acc {α : Type u_2} [has_lt α] [no_max_order α] (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

is_bot a = ∀ (b : α), a ≤ b

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

is_top a = ∀ (b : α), b ≤ a

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

is_min a = ∀ ⦃b : α⦄, b ≤ a → a ≤ b

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

is_max a = ∀ ⦃b : α⦄, a ≤ b → b ≤ a

@[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 : α} :

is_bot (⇑order_dual.to_dual a) ↔ is_top a

@[simp]

theorem is_top_to_dual_iff {α : Type u_2} [has_le α] {a : α} :

is_top (⇑order_dual.to_dual a) ↔ is_bot a

@[simp]

theorem is_min_to_dual_iff {α : Type u_2} [has_le α] {a : α} :

is_min (⇑order_dual.to_dual a) ↔ is_max a

@[simp]

theorem is_max_to_dual_iff {α : Type u_2} [has_le α] {a : α} :

is_max (⇑order_dual.to_dual a) ↔ is_min a

@[simp]

theorem is_bot_of_dual_iff {α : Type u_2} [has_le α] {a : αᵒᵈ} :

is_bot (⇑order_dual.of_dual a) ↔ is_top a

@[simp]

theorem is_top_of_dual_iff {α : Type u_2} [has_le α] {a : αᵒᵈ} :

is_top (⇑order_dual.of_dual a) ↔ is_bot a

@[simp]

theorem is_min_of_dual_iff {α : Type u_2} [has_le α] {a : αᵒᵈ} :

is_min (⇑order_dual.of_dual a) ↔ is_max a

@[simp]

theorem is_max_of_dual_iff {α : Type u_2} [has_le α] {a : αᵒᵈ} :

is_max (⇑order_dual.of_dual a) ↔ is_min a

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

is_top a → is_bot (⇑order_dual.to_dual a)

Alias of the reverse direction of is_bot_to_dual_iff.

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

is_bot a → is_top (⇑order_dual.to_dual a)

Alias of the reverse direction of is_top_to_dual_iff.

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

is_max a → is_min (⇑order_dual.to_dual a)

Alias of the reverse direction of is_min_to_dual_iff.

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

is_min a → is_max (⇑order_dual.to_dual a)

Alias of the reverse direction of is_max_to_dual_iff.

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

is_top a → is_bot (⇑order_dual.of_dual a)

Alias of the reverse direction of is_bot_of_dual_iff.

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

is_bot a → is_top (⇑order_dual.of_dual a)

Alias of the reverse direction of is_top_of_dual_iff.

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

is_max a → is_min (⇑order_dual.of_dual a)

Alias of the reverse direction of is_min_of_dual_iff.

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

is_min a → is_max (⇑order_dual.of_dual 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 : α} :

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

theorem is_max_iff_forall_not_lt {α : Type u_2} [preorder α] {a : α} :

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

@[simp]

theorem not_is_min_iff {α : Type u_2} [preorder α] {a : α} :

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

@[simp]

theorem not_is_max_iff {α : Type u_2} [preorder α] {a : α} :

¬is_max 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} [partial_order α] {a b : α} (ha : is_min a) (h : b ≤ a) :

b = a

@[protected]

theorem is_min.eq_of_ge {α : Type u_2} [partial_order α] {a b : α} (ha : is_min a) (h : b ≤ a) :

a = b

@[protected]

theorem is_max.eq_of_le {α : Type u_2} [partial_order α] {a b : α} (ha : is_max a) (h : a ≤ b) :

a = b

@[protected]

theorem is_max.eq_of_ge {α : Type u_2} [partial_order α] {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 : α × β} :

is_bot x ↔ is_bot x.fst ∧ is_bot x.snd

theorem prod.is_top_iff {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} :

is_top x ↔ is_top x.fst ∧ is_top x.snd

theorem prod.is_min_iff {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} :

is_min x ↔ is_min x.fst ∧ is_min x.snd

theorem prod.is_max_iff {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {x : α × β} :

is_max x ↔ is_max x.fst ∧ is_max x.snd