order.bounded_order - mathlib3 docs

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

Instances of this typeclass

Instances of other typeclasses for order_top

order_top.has_sizeof_inst

source

@[instance]

def order_top.to_has_top (α : Type u) [has_le α] [self : order_top α] :

has_top α

source

noncomputable def top_order_or_no_top_order (α : Type u_1) [has_le α] :

psum (order_top α) (no_top_order α)

An order is (noncomputably) either an order_top or a no_order_top. Use as casesI bot_order_or_no_bot_order α.

Equations

top_order_or_no_top_order α = dite (∀ (a : α), ∃ (b : α), ¬b ≤ a) (λ (H : ∀ (a : α), ∃ (b : α), ¬b ≤ a), psum.inr _) (λ (H : ¬∀ (a : α), ∃ (b : α), ¬b ≤ a), psum.inl {top := (classical.indefinite_description (λ (x : α), ∀ (b : α), b ≤ x) _).val, le_top := _})

source

@[simp]

theorem le_top {α : Type u} [has_le α] [order_top α] {a : α} :

a ≤ ⊤

source

@[simp]

theorem is_top_top {α : Type u} [has_le α] [order_top α] :

is_top ⊤

source

@[simp]

theorem is_max_top {α : Type u} [preorder α] [order_top α] :

is_max ⊤

source

@[simp]

theorem not_top_lt {α : Type u} [preorder α] [order_top α] {a : α} :

¬⊤ < a

source

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

a ≠ ⊤

source

theorem has_lt.lt.ne_top {α : Type u} [preorder α] [order_top α] {a b : α} (h : a < b) :

a ≠ ⊤

Alias of ne_top_of_lt.

source

@[simp]

theorem is_max_iff_eq_top {α : Type u} [partial_order α] [order_top α] {a : α} :

is_max a ↔ a = ⊤

source

@[simp]

theorem is_top_iff_eq_top {α : Type u} [partial_order α] [order_top α] {a : α} :

is_top a ↔ a = ⊤

source

theorem not_is_max_iff_ne_top {α : Type u} [partial_order α] [order_top α] {a : α} :

¬is_max a ↔ a ≠ ⊤

source

theorem not_is_top_iff_ne_top {α : Type u} [partial_order α] [order_top α] {a : α} :

¬is_top a ↔ a ≠ ⊤

source

theorem is_max.eq_top {α : Type u} [partial_order α] [order_top α] {a : α} :

is_max a → a = ⊤

Alias of the forward direction of is_max_iff_eq_top.

source

theorem is_top.eq_top {α : Type u} [partial_order α] [order_top α] {a : α} :

is_top a → a = ⊤

Alias of the forward direction of is_top_iff_eq_top.

source

@[simp]

theorem top_le_iff {α : Type u} [partial_order α] [order_top α] {a : α} :

⊤ ≤ a ↔ a = ⊤

source

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

a = ⊤

source

theorem eq_top_iff {α : Type u} [partial_order α] [order_top α] {a : α} :

a = ⊤ ↔ ⊤ ≤ a

source

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

b = ⊤

source

theorem lt_top_iff_ne_top {α : Type u} [partial_order α] [order_top α] {a : α} :

a < ⊤ ↔ a ≠ ⊤

source

@[simp]

theorem not_lt_top_iff {α : Type u} [partial_order α] [order_top α] {a : α} :

¬a < ⊤ ↔ a = ⊤

source

theorem eq_top_or_lt_top {α : Type u} [partial_order α] [order_top α] (a : α) :

a = ⊤ ∨ a < ⊤

source

theorem ne.lt_top {α : Type u} [partial_order α] [order_top α] {a : α} (h : a ≠ ⊤) :

a < ⊤

source

theorem ne.lt_top' {α : Type u} [partial_order α] [order_top α] {a : α} (h : ⊤ ≠ a) :

a < ⊤

source

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

a ≠ ⊤

source

theorem strict_mono.apply_eq_top_iff {α : Type u} {β : Type v} [partial_order α] [order_top α] [preorder β] {f : α → β} {a : α} (hf : strict_mono f) :

f a = f ⊤ ↔ a = ⊤

source

theorem strict_anti.apply_eq_top_iff {α : Type u} {β : Type v} [partial_order α] [order_top α] [preorder β] {f : α → β} {a : α} (hf : strict_anti f) :

f a = f ⊤ ↔ a = ⊤

source

theorem not_is_min_top {α : Type u} [partial_order α] [order_top α] [nontrivial α] :

¬is_min ⊤

source

theorem strict_mono.maximal_preimage_top {α : Type u} {β : Type v} [linear_order α] [preorder β] [order_top β] {f : α → β} (H : strict_mono f) {a : α} (h_top : f a = ⊤) (x : α) :

x ≤ a

source

theorem order_top.ext_top {α : Type u_1} {hA : partial_order α} (A : order_top α) {hB : partial_order α} (B : order_top α) (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

⊤ = ⊤

source

theorem order_top.ext {α : Type u_1} [partial_order α] {A B : order_top α} :

A = B

source

@[class]

structure order_bot (α : Type u) [has_le α] :

Type u

bot : α
bot_le : ∀ (a : α), ⊥ ≤ a

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

Instances of this typeclass

Instances of other typeclasses for order_bot

order_bot.has_sizeof_inst

source

@[instance]

def order_bot.to_has_bot (α : Type u) [has_le α] [self : order_bot α] :

has_bot α

source

noncomputable def bot_order_or_no_bot_order (α : Type u_1) [has_le α] :

psum (order_bot α) (no_bot_order α)

An order is (noncomputably) either an order_bot or a no_order_bot. Use as casesI bot_order_or_no_bot_order α.

Equations

bot_order_or_no_bot_order α = dite (∀ (a : α), ∃ (b : α), ¬a ≤ b) (λ (H : ∀ (a : α), ∃ (b : α), ¬a ≤ b), psum.inr _) (λ (H : ¬∀ (a : α), ∃ (b : α), ¬a ≤ b), psum.inl {bot := (classical.indefinite_description (λ (x : α), ∀ (b : α), x ≤ b) _).val, bot_le := _})

source

@[simp]

theorem bot_le {α : Type u} [has_le α] [order_bot α] {a : α} :

⊥ ≤ a

source

@[simp]

theorem is_bot_bot {α : Type u} [has_le α] [order_bot α] :

is_bot ⊥

source

@[protected, instance]

def order_dual.has_top (α : Type u) [has_bot α] :

has_top αᵒᵈ

Equations

order_dual.has_top α = {top := ⊥}

source

@[protected, instance]

def order_dual.has_bot (α : Type u) [has_top α] :

has_bot αᵒᵈ

Equations

order_dual.has_bot α = {bot := ⊤}

source

@[protected, instance]

def order_dual.order_top (α : Type u) [has_le α] [order_bot α] :

order_top αᵒᵈ

Equations

order_dual.order_top α = {top := ⊤, le_top := _}

source

@[protected, instance]

def order_dual.order_bot (α : Type u) [has_le α] [order_top α] :

order_bot αᵒᵈ

Equations

order_dual.order_bot α = {bot := ⊥, bot_le := _}

source

@[simp]

theorem order_dual.of_dual_bot (α : Type u) [has_top α] :

⇑order_dual.of_dual ⊥ = ⊤

source

@[simp]

theorem order_dual.of_dual_top (α : Type u) [has_bot α] :

⇑order_dual.of_dual ⊤ = ⊥

source

@[simp]

theorem order_dual.to_dual_bot (α : Type u) [has_bot α] :

⇑order_dual.to_dual ⊥ = ⊤

source

@[simp]

theorem order_dual.to_dual_top (α : Type u) [has_top α] :

⇑order_dual.to_dual ⊤ = ⊥

source

@[simp]

theorem is_min_bot {α : Type u} [preorder α] [order_bot α] :

is_min ⊥

source

@[simp]

theorem not_lt_bot {α : Type u} [preorder α] [order_bot α] {a : α} :

¬a < ⊥

source

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

b ≠ ⊥

source

theorem has_lt.lt.ne_bot {α : Type u} [preorder α] [order_bot α] {a b : α} (h : a < b) :

b ≠ ⊥

Alias of ne_bot_of_gt.

source

@[simp]

theorem is_min_iff_eq_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :

is_min a ↔ a = ⊥

source

@[simp]

theorem is_bot_iff_eq_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :

is_bot a ↔ a = ⊥

source

theorem not_is_min_iff_ne_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :

¬is_min a ↔ a ≠ ⊥

source

theorem not_is_bot_iff_ne_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :

¬is_bot a ↔ a ≠ ⊥

source

theorem is_min.eq_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :

is_min a → a = ⊥

Alias of the forward direction of is_min_iff_eq_bot.

source

theorem is_bot.eq_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :

is_bot a → a = ⊥

Alias of the forward direction of is_bot_iff_eq_bot.

source

@[simp]

theorem le_bot_iff {α : Type u} [partial_order α] [order_bot α] {a : α} :

a ≤ ⊥ ↔ a = ⊥

source

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

a = ⊥

source

theorem eq_bot_iff {α : Type u} [partial_order α] [order_bot α] {a : α} :

a = ⊥ ↔ a ≤ ⊥

source

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

a = ⊥

source

theorem bot_lt_iff_ne_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :

⊥ < a ↔ a ≠ ⊥

source

@[simp]

theorem not_bot_lt_iff {α : Type u} [partial_order α] [order_bot α] {a : α} :

¬⊥ < a ↔ a = ⊥

source

theorem eq_bot_or_bot_lt {α : Type u} [partial_order α] [order_bot α] (a : α) :

a = ⊥ ∨ ⊥ < a

source

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

a = ⊥

source

theorem ne.bot_lt {α : Type u} [partial_order α] [order_bot α] {a : α} (h : a ≠ ⊥) :

⊥ < a

source

theorem ne.bot_lt' {α : Type u} [partial_order α] [order_bot α] {a : α} (h : ⊥ ≠ a) :

⊥ < a

source

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

a ≠ ⊥

source

theorem strict_mono.apply_eq_bot_iff {α : Type u} {β : Type v} [partial_order α] [order_bot α] [preorder β] {f : α → β} {a : α} (hf : strict_mono f) :

f a = f ⊥ ↔ a = ⊥

source

theorem strict_anti.apply_eq_bot_iff {α : Type u} {β : Type v} [partial_order α] [order_bot α] [preorder β] {f : α → β} {a : α} (hf : strict_anti f) :

f a = f ⊥ ↔ a = ⊥

source

theorem not_is_max_bot {α : Type u} [partial_order α] [order_bot α] [nontrivial α] :

¬is_max ⊥

source

theorem strict_mono.minimal_preimage_bot {α : Type u} {β : Type v} [linear_order α] [partial_order β] [order_bot β] {f : α → β} (H : strict_mono f) {a : α} (h_bot : f a = ⊥) (x : α) :

a ≤ x

source

theorem order_bot.ext_bot {α : Type u_1} {hA : partial_order α} (A : order_bot α) {hB : partial_order α} (B : order_bot α) (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

⊥ = ⊥

source

theorem order_bot.ext {α : Type u_1} [partial_order α] {A B : order_bot α} :

A = B

source

@[simp]

theorem top_sup_eq {α : Type u} [semilattice_sup α] [order_top α] {a : α} :

⊤ ⊔ a = ⊤

source

@[simp]

theorem sup_top_eq {α : Type u} [semilattice_sup α] [order_top α] {a : α} :

a ⊔ ⊤ = ⊤

source

@[simp]

theorem bot_sup_eq {α : Type u} [semilattice_sup α] [order_bot α] {a : α} :

⊥ ⊔ a = a

source

@[simp]

theorem sup_bot_eq {α : Type u} [semilattice_sup α] [order_bot α] {a : α} :

a ⊔ ⊥ = a

source

@[simp]

theorem sup_eq_bot_iff {α : Type u} [semilattice_sup α] [order_bot α] {a b : α} :

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

source

@[simp]

theorem top_inf_eq {α : Type u} [semilattice_inf α] [order_top α] {a : α} :

⊤ ⊓ a = a

source

@[simp]

theorem inf_top_eq {α : Type u} [semilattice_inf α] [order_top α] {a : α} :

a ⊓ ⊤ = a

source

@[simp]

theorem inf_eq_top_iff {α : Type u} [semilattice_inf α] [order_top α] {a b : α} :

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

source

@[simp]

theorem bot_inf_eq {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :

⊥ ⊓ a = ⊥

source

@[simp]

theorem inf_bot_eq {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :

a ⊓ ⊥ = ⊥

source

@[instance]

def bounded_order.to_order_bot (α : Type u) [has_le α] [self : bounded_order α] :

order_bot α

source

@[instance]

def bounded_order.to_order_top (α : Type u) [has_le α] [self : bounded_order α] :

order_top α

source

@[class]

structure bounded_order (α : Type u) [has_le α] :

Type u

top : α
le_top : ∀ (a : α), a ≤ ⊤
bot : α
bot_le : ∀ (a : α), ⊥ ≤ a

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

Instances of this typeclass

Instances of other typeclasses for bounded_order

bounded_order.has_sizeof_inst

source

@[protected, instance]

def order_dual.bounded_order (α : Type u) [has_le α] [bounded_order α] :

bounded_order αᵒᵈ

Equations

order_dual.bounded_order α = {top := order_top.top (order_dual.order_top α), le_top := _, bot := order_bot.bot (order_dual.order_bot α), bot_le := _}

source

theorem bounded_order.ext {α : Type u_1} [partial_order α] {A B : bounded_order α} :

A = B

source

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

monotone (λ (x : α), p x ∧ q x)

source

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

monotone (λ (x : α), p x ∨ q x)

source

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

monotone (has_le.le x)

source

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

monotone (has_lt.lt x)

source

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

antitone (λ (_x : α), _x ≤ x)

source

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

antitone (λ (_x : α), _x < x)

source

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

monotone (λ (y : α), ∀ (x : β), P x y)

source

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

antitone (λ (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 (λ (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 (λ (y : α), ∀ (x : β), x ∈ s → P x y)

source

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

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

source

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

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

source

@[protected, instance]

def pi.has_bot {ι : Type u_3} {α' : ι → Type u_4} [Π (i : ι), has_bot (α' i)] :

has_bot (Π (i : ι), α' i)

Equations

pi.has_bot = {bot := λ (i : ι), ⊥}

source

@[simp]

theorem pi.bot_apply {ι : Type u_3} {α' : ι → Type u_4} [Π (i : ι), has_bot (α' i)] (i : ι) :

⊥ i = ⊥

source

theorem pi.bot_def {ι : Type u_3} {α' : ι → Type u_4} [Π (i : ι), has_bot (α' i)] :

⊥ = λ (i : ι), ⊥

source

@[protected, instance]

def pi.has_top {ι : Type u_3} {α' : ι → Type u_4} [Π (i : ι), has_top (α' i)] :

has_top (Π (i : ι), α' i)

Equations

pi.has_top = {top := λ (i : ι), ⊤}

source

@[simp]

theorem pi.top_apply {ι : Type u_3} {α' : ι → Type u_4} [Π (i : ι), has_top (α' i)] (i : ι) :

⊤ i = ⊤

source

theorem pi.top_def {ι : Type u_3} {α' : ι → Type u_4} [Π (i : ι), has_top (α' i)] :

⊤ = λ (i : ι), ⊤

source

@[protected, instance]

def pi.order_top {ι : Type u_3} {α' : ι → Type u_4} [Π (i : ι), has_le (α' i)] [Π (i : ι), order_top (α' i)] :

order_top (Π (i : ι), α' i)

Equations

pi.order_top = {top := ⊤, le_top := _}

source

@[protected, instance]

def pi.order_bot {ι : Type u_3} {α' : ι → Type u_4} [Π (i : ι), has_le (α' i)] [Π (i : ι), order_bot (α' i)] :

order_bot (Π (i : ι), α' i)

Equations

pi.order_bot = {bot := ⊥, bot_le := _}

source

@[protected, instance]

def pi.bounded_order {ι : Type u_3} {α' : ι → Type u_4} [Π (i : ι), has_le (α' i)] [Π (i : ι), bounded_order (α' i)] :

bounded_order (Π (i : ι), α' i)

Equations

pi.bounded_order = {top := order_top.top pi.order_top, le_top := _, bot := order_bot.bot pi.order_bot, bot_le := _}

source

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

x = ⊥

source

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

x = ⊤

source

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

subsingleton α

source

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

subsingleton α

source

theorem subsingleton_iff_bot_eq_top {α : Type u} [partial_order α] [bounded_order α] :

⊥ = ⊤ ↔ subsingleton α

source

@[reducible]

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

order_top α

Pullback an order_top.

Equations

order_top.lift f map_le map_top = {top := ⊤, le_top := _}

source

@[reducible]

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

order_bot α

Pullback an order_bot.

Equations

order_bot.lift f map_le map_bot = {bot := ⊥, bot_le := _}

source

@[reducible]

def bounded_order.lift {α : Type u} {β : Type v} [has_le α] [has_top α] [has_bot α] [has_le β] [bounded_order β] (f : α → β) (map_le : ∀ (a b : α), f a ≤ f b → a ≤ b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) :

bounded_order α

Pullback a bounded_order.

Equations