doc-next-gen

Mathlib.Order.Max

Module docstring

{"# 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. "}
NoBotOrder structure
(α : Type*) [LE α]
Full source 
/-- Order without bottom elements. -/
class NoBotOrder (α : Type*) [LE α] : Prop where
  /-- For each term `a`, there is some `b` which is either incomparable or strictly smaller. -/
  exists_not_ge (a : α) : ∃ b, ¬a ≤ b
Order without bottom elements
Informal description
An order structure on a type `α` is said to have no bottom elements if there exists no element in `α` that is less than or equal to all other elements in `α`.
NoTopOrder structure
(α : Type*) [LE α]
Full source 
/-- Order without top elements. -/
class NoTopOrder (α : Type*) [LE α] : Prop where
  /-- For each term `a`, there is some `b` which is either incomparable or strictly larger. -/
  exists_not_le (a : α) : ∃ b, ¬b ≤ a
Order without top elements
Informal description
An order structure on a type `α` is said to have no top elements if there does not exist an element that is greater than or equal to all other elements in `α`.
NoMinOrder structure
(α : Type*) [LT α]
Full source 
/-- Order without minimal elements. Sometimes called coinitial or dense. -/
class NoMinOrder (α : Type*) [LT α] : Prop where
  /-- For each term `a`, there is some strictly smaller `b`. -/
  exists_lt (a : α) : ∃ b, b < a
Order without minimal elements
Informal description
A typeclass stating that a type $\alpha$ equipped with a strict order relation $<$ has no minimal elements. This means that for any element $a \in \alpha$, there exists another element $x \in \alpha$ such that $x < a$.
NoMaxOrder structure
(α : Type*) [LT α]
Full source 
/-- Order without maximal elements. Sometimes called cofinal. -/
class NoMaxOrder (α : Type*) [LT α] : Prop where
  /-- For each term `a`, there is some strictly greater `b`. -/
  exists_gt (a : α) : ∃ b, a < b
Order without maximal elements
Informal description
An order without maximal elements, meaning that for any element \( a \) in the order, there exists another element \( x \) such that \( a < x \).
nonempty_lt instance
[LT α] [NoMinOrder α] (a : α) : Nonempty { x // x < a }
Full source 
instance nonempty_lt [LT α] [NoMinOrder α] (a : α) : Nonempty { x // x < a } :=
  nonempty_subtype.2 (exists_lt a)
Nonempty Set of Elements Below Any Element in Order Without Minimal Elements
Informal description
For any type $\alpha$ with a strict order relation $<$ and no minimal elements, and for any element $a \in \alpha$, the set $\{x \in \alpha \mid x < a\}$ is nonempty.
nonempty_gt instance
[LT α] [NoMaxOrder α] (a : α) : Nonempty { x // a < x }
Full source 
instance nonempty_gt [LT α] [NoMaxOrder α] (a : α) : Nonempty { x // a < x } :=
  nonempty_subtype.2 (exists_gt a)
Nonempty Set of Elements Above Any Element in Order Without Maximal Elements
Informal description
For any type $\alpha$ with a strict order relation $<$ and no maximal elements, and for any element $a \in \alpha$, the set $\{x \in \alpha \mid a < x\}$ is nonempty.
IsEmpty.toNoMaxOrder instance
[LT α] [IsEmpty α] : NoMaxOrder α
Full source 
instance IsEmpty.toNoMaxOrder [LT α] [IsEmpty α] : NoMaxOrder α := ⟨isEmptyElim⟩
Empty Types Have No Maximal Elements
Informal description
For any type $\alpha$ with a strict order relation $<$ that is empty, $\alpha$ has no maximal elements.
IsEmpty.toNoMinOrder instance
[LT α] [IsEmpty α] : NoMinOrder α
Full source 
instance IsEmpty.toNoMinOrder [LT α] [IsEmpty α] : NoMinOrder α := ⟨isEmptyElim⟩
Empty Types Have No Minimal Elements
Informal description
For any type $\alpha$ with a strict order relation $<$ that is empty, $\alpha$ has no minimal elements.
noMaxOrder_of_left instance
[Preorder α] [Preorder β] [NoMaxOrder α] : NoMaxOrder (α × β)
Full source 
instance noMaxOrder_of_left [Preorder α] [Preorder β] [NoMaxOrder α] : NoMaxOrder (α × β) :=
  ⟨fun ⟨a, b⟩ => by
    obtain ⟨c, h⟩ := exists_gt a
    exact ⟨(c, b), Prod.mk_lt_mk_iff_left.2 h⟩⟩
No Maximal Elements in Left Factor Implies None in Product Order
Informal description
For any preorders $\alpha$ and $\beta$, if $\alpha$ has no maximal elements, then the product order $\alpha \times \beta$ also has no maximal elements.
noMaxOrder_of_right instance
[Preorder α] [Preorder β] [NoMaxOrder β] : NoMaxOrder (α × β)
Full source 
instance noMaxOrder_of_right [Preorder α] [Preorder β] [NoMaxOrder β] : NoMaxOrder (α × β) :=
  ⟨fun ⟨a, b⟩ => by
    obtain ⟨c, h⟩ := exists_gt b
    exact ⟨(a, c), Prod.mk_lt_mk_iff_right.2 h⟩⟩
No Maximal Elements in Right Factor Implies None in Product Order
Informal description
For any preorders $\alpha$ and $\beta$, if $\beta$ has no maximal elements, then the product order $\alpha \times \beta$ also has no maximal elements.
noMinOrder_of_left instance
[Preorder α] [Preorder β] [NoMinOrder α] : NoMinOrder (α × β)
Full source 
instance noMinOrder_of_left [Preorder α] [Preorder β] [NoMinOrder α] : NoMinOrder (α × β) :=
  ⟨fun ⟨a, b⟩ => by
    obtain ⟨c, h⟩ := exists_lt a
    exact ⟨(c, b), Prod.mk_lt_mk_iff_left.2 h⟩⟩
Product Order Preserves No Minimal Elements in Left Factor
Informal description
For any preorders $\alpha$ and $\beta$, if $\alpha$ has no minimal elements, then the product order $\alpha \times \beta$ also has no minimal elements.
noMinOrder_of_right instance
[Preorder α] [Preorder β] [NoMinOrder β] : NoMinOrder (α × β)
Full source 
instance noMinOrder_of_right [Preorder α] [Preorder β] [NoMinOrder β] : NoMinOrder (α × β) :=
  ⟨fun ⟨a, b⟩ => by
    obtain ⟨c, h⟩ := exists_lt b
    exact ⟨(a, c), Prod.mk_lt_mk_iff_right.2 h⟩⟩
Product Order Preserves No Minimal Elements in Right Factor
Informal description
For any preorders $\alpha$ and $\beta$, if $\beta$ has no minimal elements, then the product order $\alpha \times \beta$ also has no minimal elements.
instNoMaxOrderForallOfNonempty instance
{ι : Type u} {π : ι → Type*} [Nonempty ι] [∀ i, Preorder (π i)] [∀ i, NoMaxOrder (π i)] : NoMaxOrder (∀ i, π i)
Full source 
instance {ι : Type u} {π : ι → Type*} [Nonempty ι] [∀ i, Preorder (π i)] [∀ i, NoMaxOrder (π i)] :
    NoMaxOrder (∀ i, π i) :=
  ⟨fun a => by
    classical
    obtain ⟨b, hb⟩ := exists_gt (a <| Classical.arbitrary _)
    exact ⟨_, lt_update_self_iff.2 hb⟩⟩
Product of Orders Without Maximal Elements Has No Maximal Elements
Informal description
For any nonempty index type $\iota$ and a family of preorders $(\pi_i)_{i \in \iota}$, if each $\pi_i$ has no maximal elements, then the product order on the function space $\forall i, \pi_i$ also has no maximal elements.
instNoMinOrderForallOfNonempty instance
{ι : Type u} {π : ι → Type*} [Nonempty ι] [∀ i, Preorder (π i)] [∀ i, NoMinOrder (π i)] : NoMinOrder (∀ i, π i)
Full source 
instance {ι : Type u} {π : ι → Type*} [Nonempty ι] [∀ i, Preorder (π i)] [∀ i, NoMinOrder (π i)] :
    NoMinOrder (∀ i, π i) :=
  ⟨fun a => by
     classical
      obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)
      exact ⟨_, update_lt_self_iff.2 hb⟩⟩
Product of Orders Without Minimal Elements Has No Minimal Elements
Informal description
For any nonempty index type $\iota$ and a family of preorders $(\pi_i)_{i \in \iota}$, if each $\pi_i$ has no minimal elements, then the product order on the function space $\forall i, \pi_i$ also has no minimal elements.
NoBotOrder.to_noMinOrder theorem
(α : Type*) [LinearOrder α] [NoBotOrder α] : NoMinOrder α
Full source 
theorem NoBotOrder.to_noMinOrder (α : Type*) [LinearOrder α] [NoBotOrder α] : NoMinOrder α :=
  { exists_lt := fun a => by simpa [not_le] using exists_not_ge a }
No Bottom Elements Implies No Minimal Elements in Linear Orders
Informal description
For any linearly ordered type $\alpha$ with no bottom elements, there are no minimal elements in $\alpha$.
NoTopOrder.to_noMaxOrder theorem
(α : Type*) [LinearOrder α] [NoTopOrder α] : NoMaxOrder α
Full source 
theorem NoTopOrder.to_noMaxOrder (α : Type*) [LinearOrder α] [NoTopOrder α] : NoMaxOrder α :=
  { exists_gt := fun a => by simpa [not_le] using exists_not_le a }
No Top Elements Implies No Maximal Elements in Linear Orders
Informal description
For any linearly ordered type $\alpha$ with no top elements, there are no maximal elements in $\alpha$.
noBotOrder_iff_noMinOrder theorem
(α : Type*) [LinearOrder α] : NoBotOrder α ↔ NoMinOrder α
Full source 
theorem noBotOrder_iff_noMinOrder (α : Type*) [LinearOrder α] : NoBotOrderNoBotOrder α ↔ NoMinOrder α :=
  ⟨fun h =>
    haveI := h
    NoBotOrder.to_noMinOrder α,
    fun h =>
    haveI := h
    inferInstance⟩
Equivalence of No Bottom Elements and No Minimal Elements in Linear Orders
Informal description
For any linearly ordered type $\alpha$, the following are equivalent: 1. $\alpha$ has no bottom elements (i.e., no element is less than or equal to all other elements). 2. $\alpha$ has no minimal elements (i.e., for every element $a \in \alpha$, there exists $x \in \alpha$ such that $x < a$).
noTopOrder_iff_noMaxOrder theorem
(α : Type*) [LinearOrder α] : NoTopOrder α ↔ NoMaxOrder α
Full source 
theorem noTopOrder_iff_noMaxOrder (α : Type*) [LinearOrder α] : NoTopOrderNoTopOrder α ↔ NoMaxOrder α :=
  ⟨fun h =>
    haveI := h
    NoTopOrder.to_noMaxOrder α,
    fun h =>
    haveI := h
    inferInstance⟩
Equivalence of No Top Elements and No Maximal Elements in Linear Orders
Informal description
For any linearly ordered type $\alpha$, the following are equivalent: 1. $\alpha$ has no top elements (i.e., no element is greater than or equal to all other elements). 2. $\alpha$ has no maximal elements (i.e., for every element $a \in \alpha$, there exists $x \in \alpha$ such that $a < x$).
NoMinOrder.not_acc theorem
[LT α] [NoMinOrder α] (a : α) : ¬Acc (· < ·) a
Full source 
theorem NoMinOrder.not_acc [LT α] [NoMinOrder α] (a : α) : ¬Acc (· < ·) a := fun h =>
  Acc.recOn h fun x _ => (exists_lt x).recOn
Non-accessibility in orders without minimal elements
Informal description
In an order without minimal elements (i.e., for every element $a$ there exists $x$ such that $x < a$), no element $a$ is accessible with respect to the less-than relation $(<)$. In other words, the relation $(<)$ is not well-founded.
NoMaxOrder.not_acc theorem
[LT α] [NoMaxOrder α] (a : α) : ¬Acc (· > ·) a
Full source 
theorem NoMaxOrder.not_acc [LT α] [NoMaxOrder α] (a : α) : ¬Acc (· > ·) a := fun h =>
  Acc.recOn h fun x _ => (exists_gt x).recOn
Non-accessibility in orders without maximal elements
Informal description
In an order without maximal elements (i.e., for every element $a$ there exists $x$ such that $a < x$), no element $a$ is accessible with respect to the greater-than relation $(>)$. In other words, the relation $(>)$ is not well-founded.
IsBot definition
(a : α) : Prop
Full source 
/-- `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. -/
def IsBot (a : α) : Prop :=
  ∀ b, a ≤ b
Bottom element in a preorder
Informal description
An element $a$ in a preorder $\alpha$ is called a *bottom element* if it is less than or equal to every other element in $\alpha$. That is, for all $b \in \alpha$, we have $a \leq b$.
IsTop definition
(a : α) : Prop
Full source 
/-- `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. -/
def IsTop (a : α) : Prop :=
  ∀ b, b ≤ a
Top element of a preorder
Informal description
An element $a$ of a preorder $\alpha$ is called a *top element* if it is greater than or equal to every other element in $\alpha$, i.e., for all $b \in \alpha$, $b \leq a$.
IsMin definition
(a : α) : Prop
Full source 
/-- `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. -/
def IsMin (a : α) : Prop :=
  ∀ ⦃b⦄, b ≤ a → a ≤ b
Minimal element in a preorder
Informal description
An element $a$ of a type $\alpha$ with a preorder is called *minimal* if for any element $b \leq a$, we have $a \leq b$. In other words, no element is strictly less than $a$.
IsMax definition
(a : α) : Prop
Full source 
/-- `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. -/
def IsMax (a : α) : Prop :=
  ∀ ⦃b⦄, a ≤ b → b ≤ a
Maximal element in a preorder
Informal description
An element \( a \) of a type \( \alpha \) with a preorder is called *maximal* if for any element \( b \) in \( \alpha \), whenever \( a \leq b \), it follows that \( b \leq a \). In other words, no element is strictly greater than \( a \).
not_isBot theorem
[NoBotOrder α] (a : α) : ¬IsBot a
Full source 
@[simp]
theorem not_isBot [NoBotOrder α] (a : α) : ¬IsBot a := fun h =>
  let ⟨_, hb⟩ := exists_not_ge a
  hb <| h _
Nonexistence of Bottom Elements in NoBotOrder
Informal description
In an order $\alpha$ with no bottom elements (i.e., a `NoBotOrder`), no element $a \in \alpha$ is a bottom element. That is, for any $a \in \alpha$, there exists some $b \in \alpha$ such that $a \nleq b$.
not_isTop theorem
[NoTopOrder α] (a : α) : ¬IsTop a
Full source 
@[simp]
theorem not_isTop [NoTopOrder α] (a : α) : ¬IsTop a := fun h =>
  let ⟨_, hb⟩ := exists_not_le a
  hb <| h _
Nonexistence of Top Elements in NoTopOrder
Informal description
In an order $\alpha$ with no top elements (i.e., a `NoTopOrder`), no element $a \in \alpha$ is a top element. That is, for any $a \in \alpha$, there exists some $b \in \alpha$ such that $a \ngeq b$.
IsBot.isMin theorem
(h : IsBot a) : IsMin a
Full source 
protected theorem IsBot.isMin (h : IsBot a) : IsMin a := fun b _ => h b
Bottom Elements are Minimal
Informal description
If an element $a$ in a preorder is a bottom element (i.e., $a \leq b$ for all $b$), then $a$ is minimal (i.e., there is no element strictly less than $a$).
IsTop.isMax theorem
(h : IsTop a) : IsMax a
Full source 
protected theorem IsTop.isMax (h : IsTop a) : IsMax a := fun b _ => h b
Top Elements are Maximal
Informal description
If an element $a$ in a preorder is a top element (i.e., $b \leq a$ for all $b$), then $a$ is maximal (i.e., for all $b$, $a \leq b$ implies $b \leq a$).
IsTop.isMax_iff theorem
{α} [PartialOrder α] {i j : α} (h : IsTop i) : IsMax j ↔ j = i
Full source 
theorem IsTop.isMax_iff {α} [PartialOrder α] {i j : α} (h : IsTop i) : IsMaxIsMax j ↔ j = i := by
  simp_rw [le_antisymm_iff, h j, true_and]
  exact ⟨(· (h j)), Function.swap (fun _ ↦ h · |>.trans ·)⟩
Maximal Elements in a Partial Order with Top are Exactly the Top Elements
Informal description
Let $\alpha$ be a partially ordered set with a top element $i$. For any element $j \in \alpha$, $j$ is maximal if and only if $j = i$.
IsBot.isMin_iff theorem
{α} [PartialOrder α] {i j : α} (h : IsBot i) : IsMin j ↔ j = i
Full source 
theorem IsBot.isMin_iff {α} [PartialOrder α] {i j : α} (h : IsBot i) : IsMinIsMin j ↔ j = i := by
  simp_rw [le_antisymm_iff, h j, and_true]
  exact ⟨fun a ↦ a (h j), fun a h' ↦ fun _ ↦ Preorder.le_trans j i h' a (h h')⟩
Characterization of Minimal Elements in a Partial Order with Bottom Element
Informal description
Let $\alpha$ be a partially ordered set with a bottom element $i$. For any element $j \in \alpha$, $j$ is minimal if and only if $j = i$.
isBot_toDual_iff theorem
: IsBot (toDual a) ↔ IsTop a
Full source 
@[simp]
theorem isBot_toDual_iff : IsBotIsBot (toDual a) ↔ IsTop a :=
  Iff.rfl
Duality Between Bottom and Top Elements via Order Reversal
Informal description
For any element $a$ in a preorder $\alpha$, the element $\text{toDual}(a)$ is a bottom element in the dual order if and only if $a$ is a top element in the original order. That is, $\text{toDual}(a) \leq b$ for all $b$ in the dual order if and only if $a \geq b$ for all $b$ in the original order.
isTop_toDual_iff theorem
: IsTop (toDual a) ↔ IsBot a
Full source 
@[simp]
theorem isTop_toDual_iff : IsTopIsTop (toDual a) ↔ IsBot a :=
  Iff.rfl
Duality Between Top and Bottom Elements via Order Reversal
Informal description
For any element $a$ in a preorder $\alpha$, the element $\text{toDual}(a)$ is a top element in the dual order if and only if $a$ is a bottom element in the original order. That is, $\text{toDual}(a)$ is greater than or equal to every other element in the dual order if and only if $a$ is less than or equal to every other element in the original order.
isMin_toDual_iff theorem
: IsMin (toDual a) ↔ IsMax a
Full source 
@[simp]
theorem isMin_toDual_iff : IsMinIsMin (toDual a) ↔ IsMax a :=
  Iff.rfl
Duality Between Minimal and Maximal Elements via Order Reversal
Informal description
For any element $a$ in a preorder $\alpha$, the element $\text{toDual}(a)$ is minimal in the dual order if and only if $a$ is maximal in the original order. In other words, no element is strictly less than $\text{toDual}(a)$ in the dual order if and only if no element is strictly greater than $a$ in the original order.
isMax_toDual_iff theorem
: IsMax (toDual a) ↔ IsMin a
Full source 
@[simp]
theorem isMax_toDual_iff : IsMaxIsMax (toDual a) ↔ IsMin a :=
  Iff.rfl
Duality Between Maximal and Minimal Elements via Order Reversal
Informal description
For any element $a$ in a preorder $\alpha$, the element $\text{toDual}(a)$ is maximal in the dual order if and only if $a$ is minimal in the original order. In other words, no element is strictly greater than $\text{toDual}(a)$ in the dual order if and only if no element is strictly less than $a$ in the original order.
isBot_ofDual_iff theorem
{a : αᵒᵈ} : IsBot (ofDual a) ↔ IsTop a
Full source 
@[simp]
theorem isBot_ofDual_iff {a : αᵒᵈ} : IsBotIsBot (ofDual a) ↔ IsTop a :=
  Iff.rfl
Duality Between Bottom and Top Elements in Order Dual
Informal description
For any element $a$ in the order dual $\alpha^{\text{op}}$, the element $\text{ofDual}(a)$ is a bottom element in $\alpha$ if and only if $a$ is a top element in $\alpha^{\text{op}}$.
isTop_ofDual_iff theorem
{a : αᵒᵈ} : IsTop (ofDual a) ↔ IsBot a
Full source 
@[simp]
theorem isTop_ofDual_iff {a : αᵒᵈ} : IsTopIsTop (ofDual a) ↔ IsBot a :=
  Iff.rfl
Duality Between Top and Bottom Elements in Order Dual
Informal description
For any element $a$ in the order dual $\alpha^{\text{op}}$, the element $\text{ofDual}(a)$ is a top element in $\alpha$ if and only if $a$ is a bottom element in $\alpha^{\text{op}}$.
isMin_ofDual_iff theorem
{a : αᵒᵈ} : IsMin (ofDual a) ↔ IsMax a
Full source 
@[simp]
theorem isMin_ofDual_iff {a : αᵒᵈ} : IsMinIsMin (ofDual a) ↔ IsMax a :=
  Iff.rfl
Duality Between Minimal and Maximal Elements in Order Dual
Informal description
For any element $a$ in the order dual $\alpha^{\text{op}}$, the element $\text{ofDual}(a)$ is minimal in $\alpha$ if and only if $a$ is maximal in $\alpha^{\text{op}}$.
isMax_ofDual_iff theorem
{a : αᵒᵈ} : IsMax (ofDual a) ↔ IsMin a
Full source 
@[simp]
theorem isMax_ofDual_iff {a : αᵒᵈ} : IsMaxIsMax (ofDual a) ↔ IsMin a :=
  Iff.rfl
Duality Between Maximal and Minimal Elements in Order Dual
Informal description
For any element $a$ in the order dual $\alpha^{\text{op}}$, the element $\text{ofDual}(a)$ is maximal in $\alpha$ if and only if $a$ is minimal in $\alpha^{\text{op}}$.
IsBot.mono theorem
(ha : IsBot a) (h : b ≤ a) : IsBot b
Full source 
theorem IsBot.mono (ha : IsBot a) (h : b ≤ a) : IsBot b := fun _ => h.trans <| ha _
Monotonicity of Bottom Elements: $b \leq a$ Preserves Bottomness
Informal description
Let $a$ be a bottom element in a preorder (i.e., $a \leq x$ for all $x$). If $b \leq a$, then $b$ is also a bottom element.
IsTop.mono theorem
(ha : IsTop a) (h : a ≤ b) : IsTop b
Full source 
theorem IsTop.mono (ha : IsTop a) (h : a ≤ b) : IsTop b := fun _ => (ha _).trans h
Monotonicity of Top Elements: $a \leq b$ Preserves Topness
Informal description
Let $a$ be a top element in a preorder (i.e., $a \geq x$ for all $x$). If $a \leq b$, then $b$ is also a top element.
IsMin.mono theorem
(ha : IsMin a) (h : b ≤ a) : IsMin b
Full source 
theorem IsMin.mono (ha : IsMin a) (h : b ≤ a) : IsMin b := fun _ hc => h.trans <| ha <| hc.trans h
Monotonicity of Minimal Elements: $b \leq a$ Preserves Minimality
Informal description
Let $a$ be a minimal element in a preorder (i.e., no element is strictly less than $a$). If $b \leq a$, then $b$ is also a minimal element.
IsMax.mono theorem
(ha : IsMax a) (h : a ≤ b) : IsMax b
Full source 
theorem IsMax.mono (ha : IsMax a) (h : a ≤ b) : IsMax b := fun _ hc => (ha <| h.trans hc).trans h
Monotonicity of Maximal Elements: $a \leq b$ Preserves Maximality
Informal description
Let $a$ be a maximal element in a preorder (i.e., no element is strictly greater than $a$). If $a \leq b$, then $b$ is also a maximal element.
IsMin.not_lt theorem
(h : IsMin a) : ¬b < a
Full source 
theorem IsMin.not_lt (h : IsMin a) : ¬b < a := fun hb => hb.not_le <| h hb.le
No Strictly Smaller Element for Minimal Elements
Informal description
If an element $a$ is minimal in a preorder, then there does not exist any element $b$ such that $b < a$.
IsMax.not_lt theorem
(h : IsMax a) : ¬a < b
Full source 
theorem IsMax.not_lt (h : IsMax a) : ¬a < b := fun hb => hb.not_le <| h hb.le
Maximal elements have no strict successors
Informal description
If an element $a$ is maximal in a preorder, then there does not exist any element $b$ such that $a < b$.
not_isMin_of_lt theorem
(h : b < a) : ¬IsMin a
Full source 
@[simp]
theorem not_isMin_of_lt (h : b < a) : ¬IsMin a := fun ha => ha.not_lt h
Existence of a Smaller Element Implies Non-Minimality
Informal description
If there exists an element $b$ such that $b < a$ in a preorder, then $a$ is not a minimal element.
not_isMax_of_lt theorem
(h : a < b) : ¬IsMax a
Full source 
@[simp]
theorem not_isMax_of_lt (h : a < b) : ¬IsMax a := fun ha => ha.not_lt h
Existence of a Greater Element Implies Non-Maximality
Informal description
If an element $a$ is strictly less than another element $b$ in a preorder, then $a$ is not a maximal element.
not_isMin theorem
[NoMinOrder α] (a : α) : ¬IsMin a
Full source 
@[simp]
theorem not_isMin [NoMinOrder α] (a : α) : ¬IsMin a :=
  not_isMin_iff.2 <| exists_lt a
No Minimal Elements Implies No Element is Minimal
Informal description
In a preorder $\alpha$ with no minimal elements (i.e., `NoMinOrder α`), no element $a \in \alpha$ is minimal.
not_isMax theorem
[NoMaxOrder α] (a : α) : ¬IsMax a
Full source 
@[simp]
theorem not_isMax [NoMaxOrder α] (a : α) : ¬IsMax a :=
  not_isMax_iff.2 <| exists_gt a
No Maximal Elements Implies No Element is Maximal
Informal description
In a preorder $\alpha$ with no maximal elements (i.e., a `NoMaxOrder`), no element $a \in \alpha$ is maximal.
Subsingleton.isBot theorem
(a : α) : IsBot a
Full source 
protected theorem isBot (a : α) : IsBot a := fun _ => (Subsingleton.elim _ _).le
Every Element is Bottom in a Subsingleton Preorder
Informal description
In a preorder $\alpha$ that is a subsingleton (i.e., all elements are equal), every element $a \in \alpha$ is a bottom element. That is, for all $b \in \alpha$, we have $a \leq b$.
Subsingleton.isTop theorem
(a : α) : IsTop a
Full source 
protected theorem isTop (a : α) : IsTop a := fun _ => (Subsingleton.elim _ _).le
Every Element is Top in a Subsingleton Preorder
Informal description
In a preorder $\alpha$ that is a subsingleton (i.e., all elements are equal), every element $a \in \alpha$ is a top element. That is, for all $b \in \alpha$, we have $b \leq a$.
Subsingleton.isMin theorem
(a : α) : IsMin a
Full source 
protected theorem isMin (a : α) : IsMin a :=
  (Subsingleton.isBot _).isMin
Every Element is Minimal in a Subsingleton Preorder
Informal description
In a preorder $\alpha$ that is a subsingleton (i.e., all elements are equal), every element $a \in \alpha$ is minimal. That is, for all $b \in \alpha$, if $b \leq a$ then $a \leq b$.
Subsingleton.isMax theorem
(a : α) : IsMax a
Full source 
protected theorem isMax (a : α) : IsMax a :=
  (Subsingleton.isTop _).isMax
Every Element is Maximal in a Subsingleton Preorder
Informal description
In a preorder $\alpha$ that is a subsingleton (i.e., all elements are equal), every element $a \in \alpha$ is maximal. That is, for all $b \in \alpha$, if $a \leq b$ then $b \leq a$.
IsBot.lt_of_ne theorem
(ha : IsBot a) (h : a ≠ b) : a < b
Full source 
protected theorem IsBot.lt_of_ne (ha : IsBot a) (h : a ≠ b) : a < b :=
  (ha b).lt_of_ne h
Bottom Element is Strictly Less than Any Distinct Element
Informal description
Let $a$ be a bottom element in a preorder $\alpha$ (i.e., $a \leq b$ for all $b \in \alpha$). If $a \neq b$, then $a$ is strictly less than $b$, i.e., $a < b$.
IsTop.lt_of_ne theorem
(ha : IsTop a) (h : b ≠ a) : b < a
Full source 
protected theorem IsTop.lt_of_ne (ha : IsTop a) (h : b ≠ a) : b < a :=
  (ha b).lt_of_ne h
Elements Below Top Are Strictly Less
Informal description
Let $a$ be a top element in a preorder $\alpha$. For any element $b \in \alpha$ such that $b \neq a$, it follows that $b < a$.
IsBot.not_isMax theorem
[Nontrivial α] (ha : IsBot a) : ¬IsMax a
Full source 
protected theorem IsBot.not_isMax [Nontrivial α] (ha : IsBot a) : ¬ IsMax a := by
  intro ha'
  obtain ⟨b, hb⟩ := exists_ne a
  exact hb <| ha'.eq_of_ge (ha.lt_of_ne hb.symm).le
Bottom Element Cannot Be Maximal in Nontrivial Preorder
Informal description
In a nontrivial preorder $\alpha$, if an element $a$ is a bottom element (i.e., $a \leq b$ for all $b \in \alpha$), then $a$ cannot be a maximal element (i.e., there exists some $b \in \alpha$ such that $a < b$).
IsTop.not_isMin theorem
[Nontrivial α] (ha : IsTop a) : ¬IsMin a
Full source 
protected theorem IsTop.not_isMin [Nontrivial α] (ha : IsTop a) : ¬ IsMin a :=
  ha.toDual.not_isMax
Top Element Cannot Be Minimal in Nontrivial Preorder
Informal description
In a nontrivial preorder $\alpha$, if an element $a$ is a top element (i.e., $b \leq a$ for all $b \in \alpha$), then $a$ cannot be a minimal element (i.e., there exists some $b \in \alpha$ such that $b < a$).
IsBot.not_isTop theorem
[Nontrivial α] (ha : IsBot a) : ¬IsTop a
Full source 
protected theorem IsBot.not_isTop [Nontrivial α] (ha : IsBot a) : ¬ IsTop a :=
  mt IsTop.isMax ha.not_isMax
Bottom Element Cannot Be Top in Nontrivial Preorder
Informal description
In a nontrivial preorder $\alpha$, if an element $a$ is a bottom element (i.e., $a \leq b$ for all $b \in \alpha$), then $a$ cannot be a top element (i.e., there exists some $b \in \alpha$ such that $b \not\leq a$).
IsTop.not_isBot theorem
[Nontrivial α] (ha : IsTop a) : ¬IsBot a
Full source 
protected theorem IsTop.not_isBot [Nontrivial α] (ha : IsTop a) : ¬ IsBot a :=
  ha.toDual.not_isTop
Top Element Cannot Be Bottom in Nontrivial Preorder
Informal description
In a nontrivial preorder $\alpha$, if an element $a$ is a top element (i.e., $b \leq a$ for all $b \in \alpha$), then $a$ cannot be a bottom element (i.e., there exists some $b \in \alpha$ such that $a \not\leq b$).
IsBot.prodMk theorem
(ha : IsBot a) (hb : IsBot b) : IsBot (a, b)
Full source 
theorem IsBot.prodMk (ha : IsBot a) (hb : IsBot b) : IsBot (a, b) := fun _ => ⟨ha _, hb _⟩
Bottom Element in Product Preorder
Informal description
If $a$ is a bottom element in a preorder $\alpha$ and $b$ is a bottom element in a preorder $\beta$, then the pair $(a, b)$ is a bottom element in the product preorder $\alpha \times \beta$.
IsTop.prodMk theorem
(ha : IsTop a) (hb : IsTop b) : IsTop (a, b)
Full source 
theorem IsTop.prodMk (ha : IsTop a) (hb : IsTop b) : IsTop (a, b) := fun _ => ⟨ha _, hb _⟩
Product of Top Elements is Top in Product Preorder
Informal description
Let $\alpha$ and $\beta$ be preorders with elements $a \in \alpha$ and $b \in \beta$. If $a$ is a top element in $\alpha$ and $b$ is a top element in $\beta$, then the pair $(a, b)$ is a top element in the product preorder $\alpha \times \beta$.
IsMin.prodMk theorem
(ha : IsMin a) (hb : IsMin b) : IsMin (a, b)
Full source 
theorem IsMin.prodMk (ha : IsMin a) (hb : IsMin b) : IsMin (a, b) := fun _ hc => ⟨ha hc.1, hb hc.2⟩
Minimality is Preserved Under Product Order
Informal description
Given a preorder on types $\alpha$ and $\beta$, if $a$ is a minimal element in $\alpha$ and $b$ is a minimal element in $\beta$, then the pair $(a, b)$ is a minimal element in the product order on $\alpha \times \beta$.
IsMax.prodMk theorem
(ha : IsMax a) (hb : IsMax b) : IsMax (a, b)
Full source 
theorem IsMax.prodMk (ha : IsMax a) (hb : IsMax b) : IsMax (a, b) := fun _ hc => ⟨ha hc.1, hb hc.2⟩
Maximality in Product Preorder
Informal description
Let $a$ be a maximal element in a preorder on type $\alpha$ and $b$ be a maximal element in a preorder on type $\beta$. Then the pair $(a, b)$ is a maximal element in the product preorder on $\alpha \times \beta$.
IsBot.fst theorem
(hx : IsBot x) : IsBot x.1
Full source 
theorem IsBot.fst (hx : IsBot x) : IsBot x.1 := fun c => (hx (c, x.2)).1
Projection of Bottom Element to First Component
Informal description
If an element $x$ is a bottom element in the product preorder $\alpha \times \beta$, then its first component $x.1$ is a bottom element in the preorder $\alpha$.
IsBot.snd theorem
(hx : IsBot x) : IsBot x.2
Full source 
theorem IsBot.snd (hx : IsBot x) : IsBot x.2 := fun c => (hx (x.1, c)).2
Projection of Bottom Element to Second Component
Informal description
If an element $x$ is a bottom element in a product preorder, then its second component $x.2$ is also a bottom element in its respective preorder.
IsTop.fst theorem
(hx : IsTop x) : IsTop x.1
Full source 
theorem IsTop.fst (hx : IsTop x) : IsTop x.1 := fun c => (hx (c, x.2)).1
First Component of Top Element is Top
Informal description
If an element $x$ is a top element in a product preorder, then its first component $x.1$ is a top element in the first component's preorder.
IsTop.snd theorem
(hx : IsTop x) : IsTop x.2
Full source 
theorem IsTop.snd (hx : IsTop x) : IsTop x.2 := fun c => (hx (x.1, c)).2
Second Component of Top Element is Top
Informal description
If an element $x$ is a top element in a product preorder, then its second component $x.2$ is also a top element in its respective preorder.
IsMin.fst theorem
(hx : IsMin x) : IsMin x.1
Full source 
theorem IsMin.fst (hx : IsMin x) : IsMin x.1 :=
  fun c hc => (hx <| show (c, x.2) ≤ x from (and_iff_left le_rfl).2 hc).1
Minimality is preserved under first projection in product orders
Informal description
If an element $x$ is minimal in a product preorder, then its first component $x.1$ is minimal in the first component's preorder.
IsMin.snd theorem
(hx : IsMin x) : IsMin x.2
Full source 
theorem IsMin.snd (hx : IsMin x) : IsMin x.2 :=
  fun c hc => (hx <| show (x.1, c) ≤ x from (and_iff_right le_rfl).2 hc).2
Minimality of Second Component in Product Preorder
Informal description
If an element $x$ is minimal in a product preorder, then its second component $x.2$ is also minimal.
IsMax.fst theorem
(hx : IsMax x) : IsMax x.1
Full source 
theorem IsMax.fst (hx : IsMax x) : IsMax x.1 :=
  fun c hc => (hx <| show x ≤ (c, x.2) from (and_iff_left le_rfl).2 hc).1
Maximality of First Component in Product Order
Informal description
If an element $x$ is maximal in the product order, then its first component $x.1$ is maximal in its respective order.
IsMax.snd theorem
(hx : IsMax x) : IsMax x.2
Full source 
theorem IsMax.snd (hx : IsMax x) : IsMax x.2 :=
  fun c hc => (hx <| show x ≤ (x.1, c) from (and_iff_right le_rfl).2 hc).2
Maximality of Second Component in Product Order
Informal description
If an element $x$ is maximal in the product order, then its second component $x.2$ is also maximal in its respective order.
Prod.isBot_iff theorem
: IsBot x ↔ IsBot x.1 ∧ IsBot x.2
Full source 
theorem Prod.isBot_iff : IsBotIsBot x ↔ IsBot x.1 ∧ IsBot x.2 :=
  ⟨fun hx => ⟨hx.fst, hx.snd⟩, fun h => h.1.prodMk h.2⟩
Characterization of Bottom Elements in Product Preorder
Informal description
An element $x = (x_1, x_2)$ in the product preorder $\alpha \times \beta$ is a bottom element if and only if both its first component $x_1$ is a bottom element in $\alpha$ and its second component $x_2$ is a bottom element in $\beta$.
Prod.isTop_iff theorem
: IsTop x ↔ IsTop x.1 ∧ IsTop x.2
Full source 
theorem Prod.isTop_iff : IsTopIsTop x ↔ IsTop x.1 ∧ IsTop x.2 :=
  ⟨fun hx => ⟨hx.fst, hx.snd⟩, fun h => h.1.prodMk h.2⟩
Characterization of Top Elements in Product Preorder
Informal description
An element $x = (x_1, x_2)$ in the product preorder $\alpha \times \beta$ is a top element if and only if both its first component $x_1$ is a top element in $\alpha$ and its second component $x_2$ is a top element in $\beta$.
Prod.isMin_iff theorem
: IsMin x ↔ IsMin x.1 ∧ IsMin x.2
Full source 
theorem Prod.isMin_iff : IsMinIsMin x ↔ IsMin x.1 ∧ IsMin x.2 :=
  ⟨fun hx => ⟨hx.fst, hx.snd⟩, fun h => h.1.prodMk h.2⟩
Minimality in Product Preorder: $x$ is minimal iff both components are minimal
Informal description
An element $x = (x_1, x_2)$ in the product preorder $\alpha \times \beta$ is minimal if and only if both its first component $x_1$ is minimal in $\alpha$ and its second component $x_2$ is minimal in $\beta$.
Prod.isMax_iff theorem
: IsMax x ↔ IsMax x.1 ∧ IsMax x.2
Full source 
theorem Prod.isMax_iff : IsMaxIsMax x ↔ IsMax x.1 ∧ IsMax x.2 :=
  ⟨fun hx => ⟨hx.fst, hx.snd⟩, fun h => h.1.prodMk h.2⟩
Maximality in Product Preorder: $x$ is maximal iff both components are maximal
Informal description
An element $x = (x_1, x_2)$ in the product preorder $\alpha \times \beta$ is maximal if and only if both its first component $x_1$ is maximal in $\alpha$ and its second component $x_2$ is maximal in $\beta$.