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 #

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_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

@[class]

structure no_min_order (α : Type u_2) [has_lt α] :

Prop

exists_lt : ∀ (a : α), ∃ (b : α), b < a

Order without minimal elements. Sometimes called coinitial or dense.

Instances

@[class]

structure no_max_order (α : Type u_2) [has_lt α] :

Prop

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

Order without maximal elements. Sometimes called cofinal.

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

no_bot_order (order_dual α)

@[protected, instance]

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

no_top_order (order_dual α)

@[protected, instance]

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

no_min_order (order_dual α)

@[protected, instance]

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

no_max_order (order_dual α)

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

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

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

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

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

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

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

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

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

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

is_bot (⇑order_dual.to_dual a) ↔ is_top a

@[simp]

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

is_top (⇑order_dual.to_dual a) ↔ is_bot a

@[simp]

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

is_min (⇑order_dual.to_dual a) ↔ is_max a

@[simp]

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

is_max (⇑order_dual.to_dual a) ↔ is_min a

@[simp]

theorem is_bot_of_dual_iff {α : Type u_1} [has_le α] {a : order_dual α} :

is_bot (⇑order_dual.of_dual a) ↔ is_top a

@[simp]

theorem is_top_of_dual_iff {α : Type u_1} [has_le α] {a : order_dual α} :

is_top (⇑order_dual.of_dual a) ↔ is_bot a

@[simp]

theorem is_min_of_dual_iff {α : Type u_1} [has_le α] {a : order_dual α} :

is_min (⇑order_dual.of_dual a) ↔ is_max a

@[simp]

theorem is_max_of_dual_iff {α : Type u_1} [has_le α] {a : order_dual α} :

is_max (⇑order_dual.of_dual a) ↔ is_min a

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

is_top a → is_bot (⇑order_dual.to_dual a)

Alias of is_bot_to_dual_iff.

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

is_bot a → is_top (⇑order_dual.to_dual a)

Alias of is_top_to_dual_iff.

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

is_max a → is_min (⇑order_dual.to_dual a)

Alias of is_min_to_dual_iff.

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

is_min a → is_max (⇑order_dual.to_dual a)

Alias of is_max_to_dual_iff.

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

is_top a → is_bot (⇑order_dual.of_dual a)

Alias of is_bot_of_dual_iff.

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

is_bot a → is_top (⇑order_dual.of_dual a)

Alias of is_top_of_dual_iff.

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

is_max a → is_min (⇑order_dual.of_dual a)

Alias of is_min_of_dual_iff.

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

is_min a → is_max (⇑order_dual.of_dual a)

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