mathlib3 documentation

order.bounded_order

⊤ and ⊥, bounded lattices and variants #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines top and bottom elements (greatest and least elements) of a type, the bounded variants of different kinds of lattices, sets up the typeclass hierarchy between them and provides instances for Prop and fun.

Main declarations #

Common lattices #

Top, bottom element #

@[class]
structure has_top (α : Type u) :
  • top : α

Typeclass for the (\top) notation

Instances of this typeclass
Instances of other typeclasses for has_top
  • has_top.has_sizeof_inst
@[class]
structure has_bot (α : Type u) :
  • bot : α

Typeclass for the (\bot) notation

Instances of this typeclass
Instances of other typeclasses for has_bot
  • has_bot.has_sizeof_inst
@[protected, instance]
def has_top_nonempty (α : Type u) [has_top α] :
@[protected, instance]
def has_bot_nonempty (α : Type u) [has_bot α] :
@[class]
structure order_top (α : Type u) [has_le α] :

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
@[instance]
def order_top.to_has_top (α : Type u) [has_le α] [self : order_top α] :
noncomputable def top_order_or_no_top_order (α : Type u_1) [has_le α] :

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

Equations
@[simp]
theorem le_top {α : Type u} [has_le α] [order_top α] {a : α} :
@[simp]
theorem is_top_top {α : Type u} [has_le α] [order_top α] :
@[simp]
theorem is_max_top {α : Type u} [preorder α] [order_top α] :
@[simp]
theorem not_top_lt {α : Type u} [preorder α] [order_top α] {a : α} :
theorem ne_top_of_lt {α : Type u} [preorder α] [order_top α] {a b : α} (h : a < b) :
theorem has_lt.lt.ne_top {α : Type u} [preorder α] [order_top α] {a b : α} (h : a < b) :

Alias of ne_top_of_lt.

@[simp]
theorem is_max_iff_eq_top {α : Type u} [partial_order α] [order_top α] {a : α} :
@[simp]
theorem is_top_iff_eq_top {α : Type u} [partial_order α] [order_top α] {a : α} :
theorem not_is_max_iff_ne_top {α : Type u} [partial_order α] [order_top α] {a : α} :
theorem not_is_top_iff_ne_top {α : Type u} [partial_order α] [order_top α] {a : α} :
theorem is_max.eq_top {α : Type u} [partial_order α] [order_top α] {a : α} :

Alias of the forward direction of is_max_iff_eq_top.

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

Alias of the forward direction of is_top_iff_eq_top.

@[simp]
theorem top_le_iff {α : Type u} [partial_order α] [order_top α] {a : α} :
theorem top_unique {α : Type u} [partial_order α] [order_top α] {a : α} (h : a) :
a =
theorem eq_top_iff {α : Type u} [partial_order α] [order_top α] {a : α} :
theorem eq_top_mono {α : Type u} [partial_order α] [order_top α] {a b : α} (h : a b) (h₂ : a = ) :
b =
theorem lt_top_iff_ne_top {α : Type u} [partial_order α] [order_top α] {a : α} :
@[simp]
theorem not_lt_top_iff {α : Type u} [partial_order α] [order_top α] {a : α} :
theorem eq_top_or_lt_top {α : Type u} [partial_order α] [order_top α] (a : α) :
a = a <
theorem ne.lt_top {α : Type u} [partial_order α] [order_top α] {a : α} (h : a ) :
a <
theorem ne.lt_top' {α : Type u} [partial_order α] [order_top α] {a : α} (h : a) :
a <
theorem ne_top_of_le_ne_top {α : Type u} [partial_order α] [order_top α] {a b : α} (hb : b ) (hab : a b) :
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 =
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 =
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
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) :
theorem order_top.ext {α : Type u_1} [partial_order α] {A B : order_top α} :
A = B
@[class]
structure order_bot (α : Type u) [has_le α] :

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
@[instance]
def order_bot.to_has_bot (α : Type u) [has_le α] [self : order_bot α] :
noncomputable def bot_order_or_no_bot_order (α : Type u_1) [has_le α] :

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

Equations
@[simp]
theorem bot_le {α : Type u} [has_le α] [order_bot α] {a : α} :
@[simp]
theorem is_bot_bot {α : Type u} [has_le α] [order_bot α] :
@[protected, instance]
def order_dual.has_top (α : Type u) [has_bot α] :
Equations
@[protected, instance]
def order_dual.has_bot (α : Type u) [has_top α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem is_min_bot {α : Type u} [preorder α] [order_bot α] :
@[simp]
theorem not_lt_bot {α : Type u} [preorder α] [order_bot α] {a : α} :
theorem ne_bot_of_gt {α : Type u} [preorder α] [order_bot α] {a b : α} (h : a < b) :
theorem has_lt.lt.ne_bot {α : Type u} [preorder α] [order_bot α] {a b : α} (h : a < b) :

Alias of ne_bot_of_gt.

@[simp]
theorem is_min_iff_eq_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :
@[simp]
theorem is_bot_iff_eq_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :
theorem not_is_min_iff_ne_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :
theorem not_is_bot_iff_ne_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :
theorem is_min.eq_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :

Alias of the forward direction of is_min_iff_eq_bot.

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

Alias of the forward direction of is_bot_iff_eq_bot.

@[simp]
theorem le_bot_iff {α : Type u} [partial_order α] [order_bot α] {a : α} :
theorem bot_unique {α : Type u} [partial_order α] [order_bot α] {a : α} (h : a ) :
a =
theorem eq_bot_iff {α : Type u} [partial_order α] [order_bot α] {a : α} :
theorem eq_bot_mono {α : Type u} [partial_order α] [order_bot α] {a b : α} (h : a b) (h₂ : b = ) :
a =
theorem bot_lt_iff_ne_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :
@[simp]
theorem not_bot_lt_iff {α : Type u} [partial_order α] [order_bot α] {a : α} :
theorem eq_bot_or_bot_lt {α : Type u} [partial_order α] [order_bot α] (a : α) :
a = < a
theorem eq_bot_of_minimal {α : Type u} [partial_order α] [order_bot α] {a : α} (h : (b : α), ¬b < a) :
a =
theorem ne.bot_lt {α : Type u} [partial_order α] [order_bot α] {a : α} (h : a ) :
< a
theorem ne.bot_lt' {α : Type u} [partial_order α] [order_bot α] {a : α} (h : a) :
< a
theorem ne_bot_of_le_ne_bot {α : Type u} [partial_order α] [order_bot α] {a b : α} (hb : b ) (hab : b a) :
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 =
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 =
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
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) :
theorem order_bot.ext {α : Type u_1} [partial_order α] {A B : order_bot α} :
A = B
@[simp]
theorem top_sup_eq {α : Type u} [semilattice_sup α] [order_top α] {a : α} :
@[simp]
theorem sup_top_eq {α : Type u} [semilattice_sup α] [order_top α] {a : α} :
@[simp]
theorem bot_sup_eq {α : Type u} [semilattice_sup α] [order_bot α] {a : α} :
a = a
@[simp]
theorem sup_bot_eq {α : Type u} [semilattice_sup α] [order_bot α] {a : α} :
a = a
@[simp]
theorem sup_eq_bot_iff {α : Type u} [semilattice_sup α] [order_bot α] {a b : α} :
a b = a = b =
@[simp]
theorem top_inf_eq {α : Type u} [semilattice_inf α] [order_top α] {a : α} :
a = a
@[simp]
theorem inf_top_eq {α : Type u} [semilattice_inf α] [order_top α] {a : α} :
a = a
@[simp]
theorem inf_eq_top_iff {α : Type u} [semilattice_inf α] [order_top α] {a b : α} :
a b = a = b =
@[simp]
theorem bot_inf_eq {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :
@[simp]
theorem inf_bot_eq {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :

Bounded order #

@[instance]
def bounded_order.to_order_bot (α : Type u) [has_le α] [self : bounded_order α] :
@[instance]
def bounded_order.to_order_top (α : Type u) [has_le α] [self : bounded_order α] :
@[class]
structure bounded_order (α : Type u) [has_le α] :

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
theorem bounded_order.ext {α : Type u_1} [partial_order α] {A B : bounded_order α} :
A = B

In this section we prove some properties about monotone and antitone operations on Prop #

theorem monotone_and {α : Type u} [preorder α] {p q : α Prop} (m_p : monotone p) (m_q : monotone q) :
monotone (λ (x : α), p x q x)
theorem monotone_or {α : Type u} [preorder α] {p q : α Prop} (m_p : monotone p) (m_q : monotone q) :
monotone (λ (x : α), p x q x)
theorem monotone_le {α : Type u} [preorder α] {x : α} :
theorem monotone_lt {α : Type u} [preorder α] {x : α} :
theorem antitone_le {α : Type u} [preorder α] {x : α} :
antitone (λ (_x : α), _x x)
theorem antitone_lt {α : Type u} [preorder α] {x : α} :
antitone (λ (_x : α), _x < x)
theorem monotone.forall {α : Type u} {β : Type v} [preorder α] {P : β α Prop} (hP : (x : β), monotone (P x)) :
monotone (λ (y : α), (x : β), P x y)
theorem antitone.forall {α : Type u} {β : Type v} [preorder α] {P : β α Prop} (hP : (x : β), antitone (P x)) :
antitone (λ (y : α), (x : β), P x y)
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)
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)
theorem exists_ge_and_iff_exists {α : Type u} [semilattice_sup α] {P : α Prop} {x₀ : α} (hP : monotone P) :
( (x : α), x₀ x P x) (x : α), P x
theorem exists_le_and_iff_exists {α : Type u} [semilattice_inf α] {P : α Prop} {x₀ : α} (hP : antitone P) :
( (x : α), x x₀ P x) (x : α), P x

Function lattices #

@[protected, instance]
def pi.has_bot {ι : Type u_3} {α' : ι Type u_4} [Π (i : ι), has_bot (α' i)] :
has_bot (Π (i : ι), α' i)
Equations
@[simp]
theorem pi.bot_apply {ι : Type u_3} {α' : ι Type u_4} [Π (i : ι), has_bot (α' i)] (i : ι) :
theorem pi.bot_def {ι : Type u_3} {α' : ι Type u_4} [Π (i : ι), has_bot (α' i)] :
= λ (i : ι),
@[protected, instance]
def pi.has_top {ι : Type u_3} {α' : ι Type u_4} [Π (i : ι), has_top (α' i)] :
has_top (Π (i : ι), α' i)
Equations
@[simp]
theorem pi.top_apply {ι : Type u_3} {α' : ι Type u_4} [Π (i : ι), has_top (α' i)] (i : ι) :
theorem pi.top_def {ι : Type u_3} {α' : ι Type u_4} [Π (i : ι), has_top (α' i)] :
= λ (i : ι),
@[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
@[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
@[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
theorem eq_bot_of_bot_eq_top {α : Type u} [partial_order α] [bounded_order α] (hα : = ) (x : α) :
x =
theorem eq_top_of_bot_eq_top {α : Type u} [partial_order α] [bounded_order α] (hα : = ) (x : α) :
x =
@[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 = ) :

Pullback an order_top.

Equations
@[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 = ) :

Pullback an order_bot.

Equations
@[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 = ) :

Pullback a bounded_order.

Equations

Subtype, order dual, product lattices #

@[protected, reducible]
def subtype.order_bot {α : Type u} {p : α Prop} [has_le α] [order_bot α] (hbot : p ) :
order_bot {x // p x}

A subtype remains a -order if the property holds at .

Equations
@[protected, reducible]
def subtype.order_top {α : Type u} {p : α Prop} [has_le α] [order_top α] (htop : p ) :
order_top {x // p x}

A subtype remains a -order if the property holds at .

Equations
@[protected, reducible]
def subtype.bounded_order {α : Type u} {p : α Prop} [has_le α] [bounded_order α] (hbot : p ) (htop : p ) :

A subtype remains a bounded order if the property holds at and .

Equations
@[simp]
theorem subtype.mk_bot {α : Type u} {p : α Prop} [partial_order α] [order_bot α] [order_bot (subtype p)] (hbot : p ) :
, hbot⟩ =
@[simp]
theorem subtype.mk_top {α : Type u} {p : α Prop} [partial_order α] [order_top α] [order_top (subtype p)] (htop : p ) :
, htop⟩ =
theorem subtype.coe_bot {α : Type u} {p : α Prop} [partial_order α] [order_bot α] [order_bot (subtype p)] (hbot : p ) :
theorem subtype.coe_top {α : Type u} {p : α Prop} [partial_order α] [order_top α] [order_top (subtype p)] (htop : p ) :
@[simp]
theorem subtype.coe_eq_bot_iff {α : Type u} {p : α Prop} [partial_order α] [order_bot α] [order_bot (subtype p)] (hbot : p ) {x : {x // p x}} :
@[simp]
theorem subtype.coe_eq_top_iff {α : Type u} {p : α Prop} [partial_order α] [order_top α] [order_top (subtype p)] (htop : p ) {x : {x // p x}} :
@[simp]
theorem subtype.mk_eq_bot_iff {α : Type u} {p : α Prop} [partial_order α] [order_bot α] [order_bot (subtype p)] (hbot : p ) {x : α} (hx : p x) :
x, hx⟩ = x =
@[simp]
theorem subtype.mk_eq_top_iff {α : Type u} {p : α Prop} [partial_order α] [order_top α] [order_top (subtype p)] (htop : p ) {x : α} (hx : p x) :
x, hx⟩ = x =
@[protected, instance]
def prod.has_top (α : Type u) (β : Type v) [has_top α] [has_top β] :
has_top × β)
Equations
@[protected, instance]
def prod.has_bot (α : Type u) (β : Type v) [has_bot α] [has_bot β] :
has_bot × β)
Equations
@[protected, instance]
def prod.order_top (α : Type u) (β : Type v) [has_le α] [has_le β] [order_top α] [order_top β] :
order_top × β)
Equations
@[protected, instance]
def prod.order_bot (α : Type u) (β : Type v) [has_le α] [has_le β] [order_bot α] [order_bot β] :
order_bot × β)
Equations
@[protected, instance]
def prod.bounded_order (α : Type u) (β : Type v) [has_le α] [has_le β] [bounded_order α] [bounded_order β] :
Equations
theorem min_bot_left {α : Type u} [linear_order α] [order_bot α] (a : α) :
theorem max_top_left {α : Type u} [linear_order α] [order_top α] (a : α) :
theorem min_top_left {α : Type u} [linear_order α] [order_top α] (a : α) :
theorem max_bot_left {α : Type u} [linear_order α] [order_bot α] (a : α) :
theorem min_top_right {α : Type u} [linear_order α] [order_top α] (a : α) :
theorem max_bot_right {α : Type u} [linear_order α] [order_bot α] (a : α) :
theorem min_bot_right {α : Type u} [linear_order α] [order_bot α] (a : α) :
theorem max_top_right {α : Type u} [linear_order α] [order_top α] (a : α) :
@[simp]
theorem min_eq_bot {α : Type u} [linear_order α] [order_bot α] {a b : α} :
@[simp]
theorem max_eq_top {α : Type u} [linear_order α] [order_top α] {a b : α} :
@[simp]
theorem max_eq_bot {α : Type u} [linear_order α] [order_bot α] {a b : α} :
@[simp]
theorem min_eq_top {α : Type u} [linear_order α] [order_top α] {a b : α} :
@[simp]
theorem bot_ne_top {α : Type u} [partial_order α] [bounded_order α] [nontrivial α] :
@[simp]
theorem top_ne_bot {α : Type u} [partial_order α] [bounded_order α] [nontrivial α] :
@[simp]
theorem bot_lt_top {α : Type u} [partial_order α] [bounded_order α] [nontrivial α] :
@[protected, instance]
Equations
@[simp]
theorem top_eq_tt  :
@[simp]
theorem bot_eq_ff  :