mathlib documentation

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 is_bot_iff_is_min and is_top_iff_is_max for the equivalences in a (co)directed order.

Typeclasses #

@[class]
structure no_bot_order (α : Type u_2) [has_le α] :
Prop
  • exists_not_ge : ∀ (a : α), ∃ (b : α), ¬a b

Order without bottom elements.

Instances
@[class]
structure no_top_order (α : Type u_2) [has_le α] :
Prop
  • exists_not_le : ∀ (a : α), ∃ (b : α), ¬b a

Order without top elements.

Instances
@[protected, instance]
def nonempty_lt {α : Type u_1} [has_lt α] [no_min_order α] (a : α) :
nonempty {x // x < a}
@[protected, instance]
def nonempty_gt {α : Type u_1} [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 α] :
@[protected, instance]
def order_dual.no_top_order (α : Type u_1) [has_le α] [no_bot_order α] :
@[protected, instance]
def order_dual.no_min_order (α : Type u_1) [has_lt α] [no_max_order α] :
@[protected, instance]
def order_dual.no_max_order (α : Type u_1) [has_lt α] [no_min_order α] :
@[protected, instance]
def no_min_order.to_no_bot_order (α : Type u_1) [preorder α] [no_min_order α] :
@[protected, instance]
def no_max_order.to_no_top_order (α : Type u_1) [preorder α] [no_max_order α] :
def is_bot {α : Type u_1} [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
def is_top {α : Type u_1} [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
def is_min {α : Type u_1} [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
def is_max {α : Type u_1} [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
@[simp]
theorem not_is_bot {α : Type u_1} [has_le α] [no_bot_order α] (a : α) :
@[simp]
theorem not_is_top {α : Type u_1} [has_le α] [no_top_order α] (a : α) :
@[protected]
theorem is_bot.is_min {α : Type u_1} [has_le α] {a : α} (h : is_bot a) :
@[protected]
theorem is_top.is_max {α : Type u_1} [has_le α] {a : α} (h : is_top a) :
@[simp]
theorem is_bot_to_dual_iff {α : Type u_1} [has_le α] {a : α} :
@[simp]
theorem is_top_to_dual_iff {α : Type u_1} [has_le α] {a : α} :
@[simp]
theorem is_min_to_dual_iff {α : Type u_1} [has_le α] {a : α} :
@[simp]
theorem is_max_to_dual_iff {α : Type u_1} [has_le α] {a : α} :
@[simp]
theorem is_bot_of_dual_iff {α : Type u_1} [has_le α] {a : order_dual α} :
@[simp]
theorem is_top_of_dual_iff {α : Type u_1} [has_le α] {a : order_dual α} :
@[simp]
theorem is_min_of_dual_iff {α : Type u_1} [has_le α] {a : order_dual α} :
@[simp]
theorem is_max_of_dual_iff {α : Type u_1} [has_le α] {a : order_dual α} :
theorem is_top.to_dual {α : Type u_1} [has_le α] {a : α} :

Alias of is_bot_to_dual_iff.

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

Alias of is_top_to_dual_iff.

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

Alias of is_min_to_dual_iff.

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

Alias of is_max_to_dual_iff.

theorem is_top.of_dual {α : Type u_1} [has_le α] {a : order_dual α} :

Alias of is_bot_of_dual_iff.

theorem is_bot.of_dual {α : Type u_1} [has_le α] {a : order_dual α} :

Alias of is_top_of_dual_iff.

theorem is_max.of_dual {α : Type u_1} [has_le α] {a : order_dual α} :

Alias of is_min_of_dual_iff.

theorem is_min.of_dual {α : Type u_1} [has_le α] {a : order_dual α} :

Alias of is_max_of_dual_iff.

theorem is_bot.mono {α : Type u_1} [preorder α] {a b : α} (ha : is_bot a) (h : b a) :
theorem is_top.mono {α : Type u_1} [preorder α] {a b : α} (ha : is_top a) (h : a b) :
theorem is_min.mono {α : Type u_1} [preorder α] {a b : α} (ha : is_min a) (h : b a) :
theorem is_max.mono {α : Type u_1} [preorder α] {a b : α} (ha : is_max a) (h : a b) :
theorem is_min.not_lt {α : Type u_1} [preorder α] {a b : α} (h : is_min a) :
¬b < a
theorem is_max.not_lt {α : Type u_1} [preorder α] {a b : α} (h : is_max a) :
¬a < b
@[simp]
theorem not_is_min_of_lt {α : Type u_1} [preorder α] {a b : α} (h : b < a) :
@[simp]
theorem not_is_max_of_lt {α : Type u_1} [preorder α] {a b : α} (h : a < b) :
theorem has_lt.lt.not_is_min {α : Type u_1} [preorder α] {a b : α} (h : b < a) :

Alias of not_is_min_of_lt.

theorem has_lt.lt.not_is_max {α : Type u_1} [preorder α] {a b : α} (h : a < b) :

Alias of not_is_max_of_lt.

theorem is_min_iff_forall_not_lt {α : Type u_1} [preorder α] {a : α} :
is_min a ∀ (b : α), ¬b < a
theorem is_max_iff_forall_not_lt {α : Type u_1} [preorder α] {a : α} :
is_max a ∀ (b : α), ¬a < b
@[simp]
theorem not_is_min_iff {α : Type u_1} [preorder α] {a : α} :
¬is_min a ∃ (b : α), b < a
@[simp]
theorem not_is_max_iff {α : Type u_1} [preorder α] {a : α} :
¬is_max a ∃ (b : α), a < b
@[simp]
theorem not_is_min {α : Type u_1} [preorder α] [no_min_order α] (a : α) :
@[simp]
theorem not_is_max {α : Type u_1} [preorder α] [no_max_order α] (a : α) :
@[protected]
theorem subsingleton.is_bot {α : Type u_1} [preorder α] [subsingleton α] (a : α) :
@[protected]
theorem subsingleton.is_top {α : Type u_1} [preorder α] [subsingleton α] (a : α) :
@[protected]
theorem subsingleton.is_min {α : Type u_1} [preorder α] [subsingleton α] (a : α) :
@[protected]
theorem subsingleton.is_max {α : Type u_1} [preorder α] [subsingleton α] (a : α) :
@[protected]
theorem is_min.eq_of_le {α : Type u_1} [partial_order α] {a b : α} (ha : is_min a) (h : b a) :
b = a
@[protected]
theorem is_min.eq_of_ge {α : Type u_1} [partial_order α] {a b : α} (ha : is_min a) (h : b a) :
a = b
@[protected]
theorem is_max.eq_of_le {α : Type u_1} [partial_order α] {a b : α} (ha : is_max a) (h : a b) :
a = b
@[protected]
theorem is_max.eq_of_ge {α : Type u_1} [partial_order α] {a b : α} (ha : is_max a) (h : a b) :
b = a
theorem is_top_or_exists_gt {α : Type u_1} [linear_order α] (a : α) :
is_top a ∃ (b : α), a < b
theorem is_bot_or_exists_lt {α : Type u_1} [linear_order α] (a : α) :
is_bot a ∃ (b : α), b < a