Mathlib.Order.BoundedOrder

An order is an OrderTop if it has a greatest element. We state this using a data mixin, holding the value of ⊤ and the greatest element constraint.

Instances

source

noncomputable def topOrderOrNoTopOrder (α : Type u_3) [LE α] :

OrderTop α ⊕' NoTopOrder α

An order is (noncomputably) either an OrderTop or a NoTopOrder. Use as casesI topOrderOrNoTopOrder α.

Equations

topOrderOrNoTopOrder α = if H : ∀ (a : α), ∃ b, ¬b ≤ a then PSum.inr (_ : NoTopOrder α) else PSum.inl (OrderTop.mk (_ : ∀ (b : α), b ≤ Classical.choose (_ : ∃ x, ∀ (a : α), a ≤ x)))

Instances For

source

@[simp]

theorem le_top {α : Type u} [LE α] [OrderTop α] {a : α} :

a ≤ ⊤

source

@[simp]

theorem isTop_top {α : Type u} [LE α] [OrderTop α] :

IsTop ⊤

source

@[simp]

theorem isMax_top {α : Type u} [Preorder α] [OrderTop α] :

IsMax ⊤

source

@[simp]

theorem not_top_lt {α : Type u} [Preorder α] [OrderTop α] {a : α} :

¬⊤ < a

source

theorem ne_top_of_lt {α : Type u} [Preorder α] [OrderTop α] {a : α} {b : α} (h : a < b) :

a ≠ ⊤

source

theorem LT.lt.ne_top {α : Type u} [Preorder α] [OrderTop α] {a : α} {b : α} (h : a < b) :

a ≠ ⊤

Alias of ne_top_of_lt.

source

@[simp]

theorem isMax_iff_eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :

IsMax a ↔ a = ⊤

source

@[simp]

theorem isTop_iff_eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :

IsTop a ↔ a = ⊤

source

theorem not_isMax_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :

¬IsMax a ↔ a ≠ ⊤

source

theorem not_isTop_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :

¬IsTop a ↔ a ≠ ⊤

source

theorem IsMax.eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :

IsMax a → a = ⊤

Alias of the forward direction of isMax_iff_eq_top.

source

theorem IsTop.eq_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :

IsTop a → a = ⊤

Alias of the forward direction of isTop_iff_eq_top.

source

@[simp]

theorem top_le_iff {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :

⊤ ≤ a ↔ a = ⊤

source

theorem top_unique {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : ⊤ ≤ a) :

a = ⊤

source

theorem eq_top_iff {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :

a = ⊤ ↔ ⊤ ≤ a

source

theorem eq_top_mono {α : Type u} [PartialOrder α] [OrderTop α] {a : α} {b : α} (h : a ≤ b) (h₂ : a = ⊤) :

b = ⊤

source

theorem lt_top_iff_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :

a < ⊤ ↔ a ≠ ⊤

source

@[simp]

theorem not_lt_top_iff {α : Type u} [PartialOrder α] [OrderTop α] {a : α} :

¬a < ⊤ ↔ a = ⊤

source

theorem eq_top_or_lt_top {α : Type u} [PartialOrder α] [OrderTop α] (a : α) :

a = ⊤ ∨ a < ⊤

source

theorem Ne.lt_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : a ≠ ⊤) :

a < ⊤

source

theorem Ne.lt_top' {α : Type u} [PartialOrder α] [OrderTop α] {a : α} (h : ⊤ ≠ a) :

a < ⊤

source

theorem ne_top_of_le_ne_top {α : Type u} [PartialOrder α] [OrderTop α] {a : α} {b : α} (hb : b ≠ ⊤) (hab : a ≤ b) :

a ≠ ⊤

source

theorem StrictMono.apply_eq_top_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderTop α] [Preorder β] {f : α → β} {a : α} (hf : StrictMono f) :

f a = f ⊤ ↔ a = ⊤

source

theorem StrictAnti.apply_eq_top_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderTop α] [Preorder β] {f : α → β} {a : α} (hf : StrictAnti f) :

f a = f ⊤ ↔ a = ⊤

source

theorem not_isMin_top {α : Type u} [PartialOrder α] [OrderTop α] [Nontrivial α] :

¬IsMin ⊤

source

theorem StrictMono.maximal_preimage_top {α : Type u} {β : Type v} [LinearOrder α] [Preorder β] [OrderTop β] {f : α → β} (H : StrictMono f) {a : α} (h_top : f a = ⊤) (x : α) :

x ≤ a

source

theorem OrderTop.ext_top {α : Type u_3} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α} (B : OrderTop α) (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

⊤ = ⊤

source

class OrderBot (α : Type u) [LE α] extends Bot :

Type u

bot : α
bot_le : ∀ (a : α), ⊥ ≤ a
⊥ is the least element

An order is an OrderBot if it has a least element. We state this using a data mixin, holding the value of ⊥ and the least element constraint.

Instances

source

noncomputable def botOrderOrNoBotOrder (α : Type u_3) [LE α] :

OrderBot α ⊕' NoBotOrder α

An order is (noncomputably) either an OrderBot or a NoBotOrder. Use as casesI botOrderOrNoBotOrder α.

Equations

botOrderOrNoBotOrder α = if H : ∀ (a : α), ∃ b, ¬a ≤ b then PSum.inr (_ : NoBotOrder α) else PSum.inl (OrderBot.mk (_ : ∀ (b : α), Classical.choose (_ : ∃ x, ∀ (a : α), x ≤ a) ≤ b))

Instances For

source

@[simp]

theorem bot_le {α : Type u} [LE α] [OrderBot α] {a : α} :

⊥ ≤ a

source

@[simp]

theorem isBot_bot {α : Type u} [LE α] [OrderBot α] :

IsBot ⊥

source

instance OrderDual.top (α : Type u) [Bot α] :

Top αᵒᵈ

Equations

OrderDual.top α = { top := ⊥ }

source

instance OrderDual.bot (α : Type u) [Top α] :

Bot αᵒᵈ

Equations

OrderDual.bot α = { bot := ⊤ }

source

instance OrderDual.orderTop (α : Type u) [LE α] [OrderBot α] :

OrderTop αᵒᵈ

Equations

OrderDual.orderTop α = let src := inferInstanceAs (Top αᵒᵈ); OrderTop.mk (_ : ∀ {a : α}, ⊥ ≤ a)

source

instance OrderDual.orderBot (α : Type u) [LE α] [OrderTop α] :

OrderBot αᵒᵈ

Equations

OrderDual.orderBot α = let src := inferInstanceAs (Bot αᵒᵈ); OrderBot.mk (_ : ∀ {a : α}, a ≤ ⊤)

source

@[simp]

theorem OrderDual.ofDual_bot (α : Type u) [Top α] :

↑OrderDual.ofDual ⊥ = ⊤

source

@[simp]

theorem OrderDual.ofDual_top (α : Type u) [Bot α] :

↑OrderDual.ofDual ⊤ = ⊥

source

@[simp]

theorem OrderDual.toDual_bot (α : Type u) [Bot α] :

↑OrderDual.toDual ⊥ = ⊤

source

@[simp]

theorem OrderDual.toDual_top (α : Type u) [Top α] :

↑OrderDual.toDual ⊤ = ⊥

source

@[simp]

theorem isMin_bot {α : Type u} [Preorder α] [OrderBot α] :

IsMin ⊥

source

@[simp]

theorem not_lt_bot {α : Type u} [Preorder α] [OrderBot α] {a : α} :

¬a < ⊥

source

theorem ne_bot_of_gt {α : Type u} [Preorder α] [OrderBot α] {a : α} {b : α} (h : a < b) :

b ≠ ⊥

source

theorem LT.lt.ne_bot {α : Type u} [Preorder α] [OrderBot α] {a : α} {b : α} (h : a < b) :

b ≠ ⊥

Alias of ne_bot_of_gt.

source

@[simp]

theorem isMin_iff_eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :

IsMin a ↔ a = ⊥

source

@[simp]

theorem isBot_iff_eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :

IsBot a ↔ a = ⊥

source

theorem not_isMin_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :

¬IsMin a ↔ a ≠ ⊥

source

theorem not_isBot_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :

¬IsBot a ↔ a ≠ ⊥

source

theorem IsMin.eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :

IsMin a → a = ⊥

Alias of the forward direction of isMin_iff_eq_bot.

source

theorem IsBot.eq_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :

IsBot a → a = ⊥

Alias of the forward direction of isBot_iff_eq_bot.

source

@[simp]

theorem le_bot_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :

a ≤ ⊥ ↔ a = ⊥

source

theorem bot_unique {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a ≤ ⊥) :

a = ⊥

source

theorem eq_bot_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :

a = ⊥ ↔ a ≤ ⊥

source

theorem eq_bot_mono {α : Type u} [PartialOrder α] [OrderBot α] {a : α} {b : α} (h : a ≤ b) (h₂ : b = ⊥) :

a = ⊥

source

theorem bot_lt_iff_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :

⊥ < a ↔ a ≠ ⊥

source

@[simp]

theorem not_bot_lt_iff {α : Type u} [PartialOrder α] [OrderBot α] {a : α} :

¬⊥ < a ↔ a = ⊥

source

theorem eq_bot_or_bot_lt {α : Type u} [PartialOrder α] [OrderBot α] (a : α) :

a = ⊥ ∨ ⊥ < a

source

theorem eq_bot_of_minimal {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : ∀ (b : α), ¬b < a) :

a = ⊥

source

theorem Ne.bot_lt {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : a ≠ ⊥) :

⊥ < a

source

theorem Ne.bot_lt' {α : Type u} [PartialOrder α] [OrderBot α] {a : α} (h : ⊥ ≠ a) :

⊥ < a

source

theorem ne_bot_of_le_ne_bot {α : Type u} [PartialOrder α] [OrderBot α] {a : α} {b : α} (hb : b ≠ ⊥) (hab : b ≤ a) :

a ≠ ⊥

source

theorem StrictMono.apply_eq_bot_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderBot α] [Preorder β] {f : α → β} {a : α} (hf : StrictMono f) :

f a = f ⊥ ↔ a = ⊥

source

theorem StrictAnti.apply_eq_bot_iff {α : Type u} {β : Type v} [PartialOrder α] [OrderBot α] [Preorder β] {f : α → β} {a : α} (hf : StrictAnti f) :

f a = f ⊥ ↔ a = ⊥

source

theorem not_isMax_bot {α : Type u} [PartialOrder α] [OrderBot α] [Nontrivial α] :

¬IsMax ⊥

source

theorem StrictMono.minimal_preimage_bot {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] [OrderBot β] {f : α → β} (H : StrictMono f) {a : α} (h_bot : f a = ⊥) (x : α) :

a ≤ x

source

theorem OrderBot.ext_bot {α : Type u_3} {hA : PartialOrder α} (A : OrderBot α) {hB : PartialOrder α} (B : OrderBot α) (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

⊥ = ⊥

source

theorem top_sup_eq {α : Type u} [SemilatticeSup α] [OrderTop α] {a : α} :

⊤ ⊔ a = ⊤

source

theorem sup_top_eq {α : Type u} [SemilatticeSup α] [OrderTop α] {a : α} :

a ⊔ ⊤ = ⊤

source

theorem bot_sup_eq {α : Type u} [SemilatticeSup α] [OrderBot α] {a : α} :

⊥ ⊔ a = a

source

theorem sup_bot_eq {α : Type u} [SemilatticeSup α] [OrderBot α] {a : α} :

a ⊔ ⊥ = a

source

@[simp]

theorem sup_eq_bot_iff {α : Type u} [SemilatticeSup α] [OrderBot α] {a : α} {b : α} :

a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥

source

theorem top_inf_eq {α : Type u} [SemilatticeInf α] [OrderTop α] {a : α} :

⊤ ⊓ a = a

source

theorem inf_top_eq {α : Type u} [SemilatticeInf α] [OrderTop α] {a : α} :

a ⊓ ⊤ = a

source

@[simp]

theorem inf_eq_top_iff {α : Type u} [SemilatticeInf α] [OrderTop α] {a : α} {b : α} :

a ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤

source

theorem bot_inf_eq {α : Type u} [SemilatticeInf α] [OrderBot α] {a : α} :

⊥ ⊓ a = ⊥

source

theorem inf_bot_eq {α : Type u} [SemilatticeInf α] [OrderBot α] {a : α} :

a ⊓ ⊥ = ⊥

source

class BoundedOrder (α : Type u) [LE α] extends OrderTop , OrderBot :

Type u

A bounded order describes an order (≤) with a top and bottom element, denoted ⊤ and ⊥ respectively.

Instances

source

instance OrderDual.boundedOrder (α : Type u) [LE α] [BoundedOrder α] :

BoundedOrder αᵒᵈ

Equations

OrderDual.boundedOrder α = let src := inferInstanceAs (OrderTop αᵒᵈ); let src_1 := inferInstanceAs (OrderBot αᵒᵈ); BoundedOrder.mk

source

instance OrderBot.instSubsingleton {α : Type u} [PartialOrder α] :

Subsingleton (OrderBot α)

Equations

@OrderBot.instSubsingleton = @OrderBot.instSubsingleton.proof_1

source

instance OrderTop.instSubsingleton {α : Type u} [PartialOrder α] :

Subsingleton (OrderTop α)

Equations

@OrderTop.instSubsingleton = @OrderTop.instSubsingleton.proof_1

source

instance BoundedOrder.instSubsingleton {α : Type u} [PartialOrder α] :

Subsingleton (BoundedOrder α)

Equations

@BoundedOrder.instSubsingleton = @BoundedOrder.instSubsingleton.proof_1

source

theorem monotone_and {α : Type u} [Preorder α] {p : α → Prop} {q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) :

Monotone fun x => p x ∧ q x

source

theorem monotone_or {α : Type u} [Preorder α] {p : α → Prop} {q : α → Prop} (m_p : Monotone p) (m_q : Monotone q) :

Monotone fun x => p x ∨ q x

source

theorem monotone_le {α : Type u} [Preorder α] {x : α} :

Monotone ((fun x x_1 => x ≤ x_1) x)

source

theorem monotone_lt {α : Type u} [Preorder α] {x : α} :

Monotone ((fun x x_1 => x < x_1) x)

source

theorem antitone_le {α : Type u} [Preorder α] {x : α} :

Antitone fun x => x ≤ x

source

theorem antitone_lt {α : Type u} [Preorder α] {x : α} :

Antitone fun x => x < x

source

theorem Monotone.forall {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Monotone (P x)) :

Monotone fun y => (x : β) → P x y

source

theorem Antitone.forall {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Antitone (P x)) :

Antitone fun y => (x : β) → P x y

source

theorem Monotone.ball {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} {s : Set β} (hP : ∀ (x : β), x ∈ s → Monotone (P x)) :

Monotone fun y => (x : β) → x ∈ s → P x y

source

theorem Antitone.ball {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} {s : Set β} (hP : ∀ (x : β), x ∈ s → Antitone (P x)) :

Antitone fun y => (x : β) → x ∈ s → P x y

source

theorem Monotone.exists {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Monotone (P x)) :

Monotone fun y => ∃ x, P x y

source

theorem Antitone.exists {α : Type u} {β : Type v} [Preorder α] {P : β → α → Prop} (hP : ∀ (x : β), Antitone (P x)) :

Antitone fun y => ∃ x, P x y

source

theorem forall_ge_iff {α : Type u} [Preorder α] {P : α → Prop} {x₀ : α} (hP : Monotone P) :

((x : α) → x ≥ x₀ → P x) ↔ P x₀

source

theorem forall_le_iff {α : Type u} [Preorder α] {P : α → Prop} {x₀ : α} (hP : Antitone P) :

((x : α) → x ≤ x₀ → P x) ↔ P x₀

source

theorem exists_ge_and_iff_exists {α : Type u} [SemilatticeSup α] {P : α → Prop} {x₀ : α} (hP : Monotone P) :

(∃ x, x₀ ≤ x ∧ P x) ↔ ∃ x, P x

source

theorem exists_le_and_iff_exists {α : Type u} [SemilatticeInf α] {P : α → Prop} {x₀ : α} (hP : Antitone P) :

(∃ x, x ≤ x₀ ∧ P x) ↔ ∃ x, P x

source

instance Pi.instBotForAll {ι : Type u_3} {α' : ι → Type u_4} [(i : ι) → Bot (α' i)] :

Bot ((i : ι) → α' i)

Equations

Pi.instBotForAll = { bot := fun x => ⊥ }

source

@[simp]

theorem Pi.bot_apply {ι : Type u_3} {α' : ι → Type u_4} [(i : ι) → Bot (α' i)] (i : ι) :

⊥ ((i : ι) → α' i) Pi.instBotForAll i = ⊥

source

theorem Pi.bot_def {ι : Type u_3} {α' : ι → Type u_4} [(i : ι) → Bot (α' i)] :

⊥ = fun x => ⊥

source

instance Pi.instTopForAll {ι : Type u_3} {α' : ι → Type u_4} [(i : ι) → Top (α' i)] :

Top ((i : ι) → α' i)

Equations

Pi.instTopForAll = { top := fun x => ⊤ }

source

@[simp]

theorem Pi.top_apply {ι : Type u_3} {α' : ι → Type u_4} [(i : ι) → Top (α' i)] (i : ι) :

⊤ ((i : ι) → α' i) Pi.instTopForAll i = ⊤

source

theorem Pi.top_def {ι : Type u_3} {α' : ι → Type u_4} [(i : ι) → Top (α' i)] :

⊤ = fun x => ⊤

source

instance Pi.orderTop {ι : Type u_3} {α' : ι → Type u_4} [(i : ι) → LE (α' i)] [(i : ι) → OrderTop (α' i)] :

OrderTop ((i : ι) → α' i)

Equations

Pi.orderTop = let src := inferInstanceAs (Top ((i : ι) → α' i)); OrderTop.mk (_ : ∀ (x : (i : ι) → α' i) (x_1 : ι), x x_1 ≤ ⊤)

source

instance Pi.orderBot {ι : Type u_3} {α' : ι → Type u_4} [(i : ι) → LE (α' i)] [(i : ι) → OrderBot (α' i)] :

OrderBot ((i : ι) → α' i)

Equations

Pi.orderBot = let src := inferInstanceAs (Bot ((i : ι) → α' i)); OrderBot.mk (_ : ∀ (x : (i : ι) → α' i) (x_1 : ι), ⊥ ≤ x x_1)

source

instance Pi.boundedOrder {ι : Type u_3} {α' : ι → Type u_4} [(i : ι) → LE (α' i)] [(i : ι) → BoundedOrder (α' i)] :

BoundedOrder ((i : ι) → α' i)

Equations

Pi.boundedOrder = let src := inferInstanceAs (OrderTop ((i : ι) → α' i)); let src_1 := inferInstanceAs (OrderBot ((i : ι) → α' i)); BoundedOrder.mk

source

theorem eq_bot_of_bot_eq_top {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : ⊥ = ⊤) (x : α) :

x = ⊥

source

theorem eq_top_of_bot_eq_top {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : ⊥ = ⊤) (x : α) :

x = ⊤

source

theorem subsingleton_of_top_le_bot {α : Type u} [PartialOrder α] [BoundedOrder α] (h : ⊤ ≤ ⊥) :

Subsingleton α

source

theorem subsingleton_of_bot_eq_top {α : Type u} [PartialOrder α] [BoundedOrder α] (hα : ⊥ = ⊤) :

Subsingleton α

source

theorem subsingleton_iff_bot_eq_top {α : Type u} [PartialOrder α] [BoundedOrder α] :

⊥ = ⊤ ↔ Subsingleton α

source

@[reducible]

def OrderTop.lift {α : Type u} {β : Type v} [LE α] [Top α] [LE β] [OrderTop β] (f : α → β) (map_le : ∀ (a b : α), f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤) :

OrderTop α

Pullback an OrderTop.

Equations

OrderTop.lift f map_le map_top = OrderTop.mk (_ : ∀ (a : α), a ≤ ⊤)

Instances For

source

@[reducible]

def OrderBot.lift {α : Type u} {β : Type v} [LE α] [Bot α] [LE β] [OrderBot β] (f : α → β) (map_le : ∀ (a b : α), f a ≤ f b → a ≤ b) (map_bot : f ⊥ = ⊥) :

OrderBot α

Pullback an OrderBot.

Equations

OrderBot.lift f map_le map_bot = OrderBot.mk (_ : ∀ (a : α), ⊥ ≤ a)

Instances For

source

@[reducible]

def BoundedOrder.lift {α : Type u} {β : Type v} [LE α] [Top α] [Bot α] [LE β] [BoundedOrder β] (f : α → β) (map_le : ∀ (a b : α), f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) :

BoundedOrder α

Pullback a BoundedOrder.

Equations