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.

source

ink

class NoBotOrder (α : Type u_1) [inst : LE α] :

Prop

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.

Instances

source

ink

class NoTopOrder (α : Type u_1) [inst : LE α] :

Prop

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.

Instances

source

ink

class NoMinOrder (α : Type u_1) [inst : LT α] :

Prop

For each term a, there is some strictly smaller b.
exists_lt : ∀ (a : α), ∃ b, b < a

Order without minimal elements. Sometimes called coinitial or dense.

Instances

source

ink

class NoMaxOrder (α : Type u_1) [inst : LT α] :

Prop

For each term a, there is some strictly greater b.
exists_gt : ∀ (a : α), ∃ b, a < b

Order without maximal elements. Sometimes called cofinal.

Instances

source

ink

instance nonempty_lt {α : Type u_1} [inst : LT α] [inst : NoMinOrder α] (a : α) :

Nonempty { x // x < a }

Equations

@nonempty_lt = @nonempty_lt.proof_1

source

ink

instance nonempty_gt {α : Type u_1} [inst : LT α] [inst : NoMaxOrder α] (a : α) :

Nonempty { x // a < x }

Equations

@nonempty_gt = @nonempty_gt.proof_1

source

ink

instance OrderDual.noBotOrder {α : Type u_1} [inst : LE α] [inst : NoTopOrder α] :

NoBotOrder αᵒᵈ

Equations

@OrderDual.noBotOrder = @OrderDual.noBotOrder.proof_1

source

ink

instance OrderDual.noTopOrder {α : Type u_1} [inst : LE α] [inst : NoBotOrder α] :

NoTopOrder αᵒᵈ

Equations

@OrderDual.noTopOrder = @OrderDual.noTopOrder.proof_1

source

ink

instance OrderDual.noMinOrder {α : Type u_1} [inst : LT α] [inst : NoMaxOrder α] :

NoMinOrder αᵒᵈ

Equations

@OrderDual.noMinOrder = @OrderDual.noMinOrder.proof_1

source

ink

instance OrderDual.noMaxOrder {α : Type u_1} [inst : LT α] [inst : NoMinOrder α] :

NoMaxOrder αᵒᵈ

Equations

@OrderDual.noMaxOrder = @OrderDual.noMaxOrder.proof_1

source

ink

instance instNoBotOrderToLE {α : Type u_1} [inst : Preorder α] [inst : NoMinOrder α] :

NoBotOrder α

Equations

@instNoBotOrderToLE = @instNoBotOrderToLE.proof_1

source

ink

instance instNoTopOrderToLE {α : Type u_1} [inst : Preorder α] [inst : NoMaxOrder α] :

NoTopOrder α

Equations

@instNoTopOrderToLE = @instNoTopOrderToLE.proof_1

source

ink

instance noMaxOrder_of_left {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : NoMaxOrder α] :

NoMaxOrder (α × β)

Equations

@noMaxOrder_of_left = @noMaxOrder_of_left.proof_1

source

ink

instance noMaxOrder_of_right {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : NoMaxOrder β] :

NoMaxOrder (α × β)

Equations

@noMaxOrder_of_right = @noMaxOrder_of_right.proof_1

source

ink

instance noMinOrder_of_left {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : NoMinOrder α] :

NoMinOrder (α × β)

Equations

@noMinOrder_of_left = @noMinOrder_of_left.proof_1

source

ink

instance noMinOrder_of_right {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] [inst : NoMinOrder β] :

NoMinOrder (α × β)

Equations

@noMinOrder_of_right = @noMinOrder_of_right.proof_1

source

ink

instance instNoMaxOrderForAllToLTPreorder {ι : Type u} {π : ι → Type u_1} [inst : Nonempty ι] [inst : (i : ι) → Preorder (π i)] [inst : ∀ (i : ι), NoMaxOrder (π i)] :

NoMaxOrder ((i : ι) → π i)

Equations

@instNoMaxOrderForAllToLTPreorder = @instNoMaxOrderForAllToLTPreorder.proof_1

source

ink

instance instNoMinOrderForAllToLTPreorder {ι : Type u} {π : ι → Type u_1} [inst : Nonempty ι] [inst : (i : ι) → Preorder (π i)] [inst : ∀ (i : ι), NoMinOrder (π i)] :

NoMinOrder ((i : ι) → π i)

Equations

@instNoMinOrderForAllToLTPreorder = @instNoMinOrderForAllToLTPreorder.proof_1

source

ink

theorem NoBotOrder.to_noMinOrder (α : Type u_1) [inst : LinearOrder α] [inst : NoBotOrder α] :

NoMinOrder α

source

ink

theorem NoTopOrder.to_noMaxOrder (α : Type u_1) [inst : LinearOrder α] [inst : NoTopOrder α] :

NoMaxOrder α

source

ink

theorem noBotOrder_iff_noMinOrder (α : Type u_1) [inst : LinearOrder α] :

NoBotOrder α ↔ NoMinOrder α

source

ink

theorem noTopOrder_iff_noMaxOrder (α : Type u_1) [inst : LinearOrder α] :

NoTopOrder α ↔ NoMaxOrder α

source

ink

theorem NoMinOrder.not_acc {α : Type u_1} [inst : LT α] [inst : NoMinOrder α] (a : α) :

¬Acc (fun x x_1 => x < x_1) a

source

ink

theorem NoMaxOrder.not_acc {α : Type u_1} [inst : LT α] [inst : NoMaxOrder α] (a : α) :

¬Acc (fun x x_1 => x > x_1) a

source

ink

def IsBot {α : Type u_1} [inst : 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

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

source

ink

def IsTop {α : Type u_1} [inst : 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

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

source

ink

def IsMin {α : Type u_1} [inst : 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

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

source

ink

def IsMax {α : Type u_1} [inst : 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