mathlib documentation

order.bounded_lattice

@[class]
structure order_top  :
Type uType u
  • top : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_top : ∀ (a : α), a

An order_top is a partial order with a maximal element. (We could state this on preorders, but then it wouldn't be unique so distinguishing one would seem odd.)

Instances
@[instance]
def order_top.to_partial_order (α : Type u) [s : order_top α] :

@[instance]
def order_top.to_has_top (α : Type u) [s : order_top α] :

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

theorem top_unique {α : Type u} [order_top α] {a : α} :
aa =

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

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

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

theorem eq_top_mono {α : Type u} [order_top α] {a b : α} :
a ba = b =

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

theorem ne_top_of_lt {α : Type u} [order_top α] {a b : α} :
a < ba

theorem ne_top_of_le_ne_top {α : Type u} [order_top α] {a b : α} :
b a ba

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

theorem order_top.ext_top {α : Type u_1} {A B : order_top α} :
(∀ (x y : α), x y x y) =

theorem order_top.ext {α : Type u_1} {A B : order_top α} :
(∀ (x y : α), x y x y)A = B

@[class]
structure order_bot  :
Type uType u
  • bot : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • bot_le : ∀ (a : α), a

An order_bot is a partial order with a minimal element. (We could state this on preorders, but then it wouldn't be unique so distinguishing one would seem odd.)

Instances
@[instance]
def order_bot.to_partial_order (α : Type u) [s : order_bot α] :

@[instance]
def order_bot.to_has_bot (α : Type u) [s : order_bot α] :

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

theorem bot_unique {α : Type u} [order_bot α] {a : α} :
a a =

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

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

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

theorem ne_bot_of_le_ne_bot {α : Type u} [order_bot α] {a b : α} :
b b aa

theorem eq_bot_mono {α : Type u} [order_bot α] {a b : α} :
a bb = a =

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

theorem ne_bot_of_gt {α : Type u} [order_bot α] {a b : α} :
a < bb

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

theorem order_bot.ext_bot {α : Type u_1} {A B : order_bot α} :
(∀ (x y : α), x y x y) =

theorem order_bot.ext {α : Type u_1} {A B : order_bot α} :
(∀ (x y : α), x y x y)A = B

@[class]
structure semilattice_sup_top  :
Type uType u
  • top : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_top : ∀ (a : α), a
  • sup : α → α → α
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c_1 : α), a c_1b c_1a b c_1

A semilattice_sup_top is a semilattice with top and join.

Instances
@[instance]

@[simp]
theorem top_sup_eq {α : Type u} [semilattice_sup_top α] {a : α} :

@[simp]
theorem sup_top_eq {α : Type u} [semilattice_sup_top α] {a : α} :

@[instance]

@[class]
structure semilattice_sup_bot  :
Type uType u
  • bot : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • bot_le : ∀ (a : α), a
  • sup : α → α → α
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c_1 : α), a c_1b c_1a b c_1

A semilattice_sup_bot is a semilattice with bottom and join.

Instances
@[simp]
theorem bot_sup_eq {α : Type u} [semilattice_sup_bot α] {a : α} :
a = a

@[simp]
theorem sup_bot_eq {α : Type u} [semilattice_sup_bot α] {a : α} :
a = a

@[simp]
theorem sup_eq_bot_iff {α : Type u} [semilattice_sup_bot α] {a b : α} :
a b = a = b =

@[class]
structure semilattice_inf_top  :
Type uType u
  • top : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_top : ∀ (a : α), a
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c_1 : α), a ba c_1a b c_1

A semilattice_inf_top is a semilattice with top and meet.

Instances
@[instance]

@[simp]
theorem top_inf_eq {α : Type u} [semilattice_inf_top α] {a : α} :
a = a

@[simp]
theorem inf_top_eq {α : Type u} [semilattice_inf_top α] {a : α} :
a = a

@[simp]
theorem inf_eq_top_iff {α : Type u} [semilattice_inf_top α] {a b : α} :
a b = a = b =

@[instance]

@[class]
structure semilattice_inf_bot  :
Type uType u
  • bot : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • bot_le : ∀ (a : α), a
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c_1 : α), a ba c_1a b c_1

A semilattice_inf_bot is a semilattice with bottom and meet.

Instances
@[simp]
theorem bot_inf_eq {α : Type u} [semilattice_inf_bot α] {a : α} :

@[simp]
theorem inf_bot_eq {α : Type u} [semilattice_inf_bot α] {a : α} :

@[instance]
def bounded_lattice.to_order_top (α : Type u) [s : bounded_lattice α] :

@[instance]
def bounded_lattice.to_order_bot (α : Type u) [s : bounded_lattice α] :

@[instance]
def bounded_lattice.to_lattice (α : Type u) [s : bounded_lattice α] :

@[class]
structure bounded_lattice  :
Type uType u
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c_1 : α), a c_1b c_1a b c_1
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c_1 : α), a ba c_1a b c_1
  • top : α
  • le_top : ∀ (a : α), a
  • bot : α
  • bot_le : ∀ (a : α), a

A bounded lattice is a lattice with a top and bottom element, denoted and respectively. This allows for the interpretation of all finite suprema and infima, taking inf ∅ = ⊤ and sup ∅ = ⊥.

Instances
theorem bounded_lattice.ext {α : Type u_1} {A B : bounded_lattice α} :
(∀ (x y : α), x y x y)A = B

@[class]
structure bounded_distrib_lattice  :
Type u_1Type u_1
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c_1 : α), a c_1b c_1a b c_1
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c_1 : α), a ba c_1a b c_1
  • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z
  • top : α
  • le_top : ∀ (a : α), a
  • bot : α
  • bot_le : ∀ (a : α), a

A bounded distributive lattice is exactly what it sounds like.

Instances
theorem inf_eq_bot_iff_le_compl {α : Type u} [bounded_distrib_lattice α] {a b c : α} :
b c = b c = (a b = a c)

@[instance]

Equations
@[instance]

Equations
@[simp]
theorem le_iff_imp {p q : Prop} :
p q p → q

theorem monotone_and {α : Type u} [preorder α] {p q : α → Prop} :
monotone pmonotone qmonotone (λ (x : α), p x q x)

theorem monotone_or {α : Type u} [preorder α] {p q : α → Prop} :
monotone pmonotone qmonotone (λ (x : α), p x q x)

@[instance]
def pi.order_bot {α : Type u_1} {β : α → Type u_2} [Π (a : α), order_bot (β a)] :
order_bot (Π (a : α), β a)

Equations
@[instance]
def pi.has_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_sup (α i)] :
has_sup (Π (i : ι), α i)

Equations
@[simp]
theorem sup_apply {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_sup (α i)] (f g : Π (i : ι), α i) (i : ι) :
(f g) i = f i g i

@[instance]
def pi.has_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_inf (α i)] :
has_inf (Π (i : ι), α i)

Equations
@[simp]
theorem inf_apply {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_inf (α i)] (f g : Π (i : ι), α i) (i : ι) :
(f g) i = f i g i

@[instance]
def pi.has_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_bot (α i)] :
has_bot (Π (i : ι), α i)

Equations
@[simp]
theorem bot_apply {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_bot (α i)] (i : ι) :

@[instance]
def pi.has_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_top (α i)] :
has_top (Π (i : ι), α i)

Equations
@[simp]
theorem top_apply {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_top (α i)] (i : ι) :

@[simp]
theorem pi.semilattice_sup_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
semilattice_sup.sup a a_1 i = (a a_1) i

@[instance]
def pi.semilattice_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup (α i)] :
semilattice_sup (Π (i : ι), α i)

Equations
@[simp]
theorem pi.semilattice_sup_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup (α i)] (a a_1 : Π (i : ι), α i) :
a a_1 = partial_order.le a a_1

@[simp]
theorem pi.semilattice_sup_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = partial_order.lt a a_1

@[simp]
theorem pi.semilattice_inf_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
semilattice_inf.inf a a_1 i = (a a_1) i

@[instance]
def pi.semilattice_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf (α i)] :
semilattice_inf (Π (i : ι), α i)

Equations
@[simp]
theorem pi.semilattice_inf_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = partial_order.lt a a_1

@[simp]
theorem pi.semilattice_inf_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf (α i)] (a a_1 : Π (i : ι), α i) :
a a_1 = partial_order.le a a_1

@[simp]
theorem pi.semilattice_inf_bot_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_bot (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
semilattice_inf_bot.inf a a_1 i = (a a_1) i

@[simp]
theorem pi.semilattice_inf_bot_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_bot (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = partial_order.lt a a_1

@[instance]
def pi.semilattice_inf_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_bot (α i)] :
semilattice_inf_bot (Π (i : ι), α i)

Equations
@[simp]
theorem pi.semilattice_inf_bot_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_bot (α i)] (i : ι) :

@[simp]
theorem pi.semilattice_inf_bot_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_bot (α i)] (a a_1 : Π (i : ι), α i) :
a a_1 = partial_order.le a a_1

@[simp]
theorem pi.semilattice_inf_top_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_top (α i)] (a a_1 : Π (i : ι), α i) :
a a_1 = partial_order.le a a_1

@[instance]
def pi.semilattice_inf_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_top (α i)] :
semilattice_inf_top (Π (i : ι), α i)

Equations
@[simp]
theorem pi.semilattice_inf_top_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_top (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = partial_order.lt a a_1

@[simp]
theorem pi.semilattice_inf_top_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_top (α i)] (i : ι) :

@[simp]
theorem pi.semilattice_inf_top_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_top (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
semilattice_inf_top.inf a a_1 i = (a a_1) i

@[simp]
theorem pi.semilattice_sup_bot_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_bot (α i)] (a a_1 : Π (i : ι), α i) :
a a_1 = partial_order.le a a_1

@[simp]
theorem pi.semilattice_sup_bot_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_bot (α i)] (i : ι) :

@[simp]
theorem pi.semilattice_sup_bot_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_bot (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
semilattice_sup_bot.sup a a_1 i = (a a_1) i

@[simp]
theorem pi.semilattice_sup_bot_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_bot (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = partial_order.lt a a_1

@[instance]
def pi.semilattice_sup_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_bot (α i)] :
semilattice_sup_bot (Π (i : ι), α i)

Equations
@[simp]
theorem pi.semilattice_sup_top_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_top (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
semilattice_sup_top.sup a a_1 i = (a a_1) i

@[simp]
theorem pi.semilattice_sup_top_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_top (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = partial_order.lt a a_1

@[instance]
def pi.semilattice_sup_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_top (α i)] :
semilattice_sup_top (Π (i : ι), α i)

Equations
@[simp]
theorem pi.semilattice_sup_top_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_top (α i)] (a a_1 : Π (i : ι), α i) :
a a_1 = partial_order.le a a_1

@[simp]
theorem pi.semilattice_sup_top_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_top (α i)] (i : ι) :

@[simp]
theorem pi.lattice_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), lattice (α i)] (a a_1 : Π (i : ι), α i) :

@[instance]
def pi.lattice {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), lattice (α i)] :
lattice (Π (i : ι), α i)

Equations
@[simp]
theorem pi.lattice_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), lattice (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :

@[simp]
theorem pi.lattice_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), lattice (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = semilattice_sup.lt a a_1

@[simp]
theorem pi.lattice_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), lattice (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :

@[simp]
theorem pi.bounded_lattice_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :

@[simp]
theorem pi.bounded_lattice_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] (i : ι) :

@[simp]
theorem pi.bounded_lattice_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :

@[simp]
theorem pi.bounded_lattice_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] (i : ι) :

@[simp]
theorem pi.bounded_lattice_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] (a a_1 : Π (i : ι), α i) :

@[simp]
theorem pi.bounded_lattice_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] (a a_1 : Π (i : ι), α i) :

theorem eq_bot_of_bot_eq_top {α : Type u_1} [bounded_lattice α] (hα : = ) (x : α) :
x =

theorem eq_top_of_bot_eq_top {α : Type u_1} [bounded_lattice α] (hα : = ) (x : α) :
x =

theorem subsingleton_of_top_le_bot {α : Type u_1} [bounded_lattice α] :

theorem subsingleton_of_bot_eq_top {α : Type u_1} [bounded_lattice α] :

def with_bot  :
Type u_1Type u_1

Attach to a type.

Equations
@[instance]
meta def with_bot.has_to_format {α : Type u_1} [has_to_format α] :

@[instance]
def with_bot.has_coe_t {α : Type u} :

Equations
@[instance]
def with_bot.has_bot {α : Type u} :

Equations
@[instance]
def with_bot.inhabited {α : Type u} :

Equations
theorem with_bot.none_eq_bot {α : Type u} :

theorem with_bot.some_eq_coe {α : Type u} (a : α) :

def with_bot.rec_bot_coe {α : Type u} {C : with_bot αSort u_1} (h₁ : C ) (h₂ : Π (a : α), C a) (n : with_bot α) :
C n

Recursor for with_bot using the preferred forms and ↑a.

Equations
theorem with_bot.coe_eq_coe {α : Type u} {a b : α} :
a = b a = b

@[instance]
def with_bot.has_lt {α : Type u} [has_lt α] :

Equations
@[simp]
theorem with_bot.some_lt_some {α : Type u} [has_lt α] {a b : α} :
some a < some b a < b

theorem with_bot.bot_lt_some {α : Type u} [has_lt α] (a : α) :

theorem with_bot.bot_lt_coe {α : Type u} [has_lt α] (a : α) :

@[instance]
def with_bot.preorder {α : Type u} [preorder α] :

Equations
@[simp]
theorem with_bot.coe_le_coe {α : Type u} [partial_order α] {a b : α} :
a b a b

@[simp]
theorem with_bot.some_le_some {α : Type u} [partial_order α] {a b : α} :
some a some b a b

theorem with_bot.coe_le {α : Type u} [partial_order α] {a b : α} {o : option α} :
b o(a o a b)

theorem with_bot.coe_lt_coe {α : Type u} [partial_order α] {a b : α} :
a < b a < b

theorem with_bot.le_coe_get_or_else {α : Type u} [preorder α] (a : with_bot α) (b : α) :

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
theorem with_bot.sup_eq_max {α : Type u} [decidable_linear_order α] (x y : with_bot α) :
x y = max x y

theorem with_bot.inf_eq_min {α : Type u} [decidable_linear_order α] (x y : with_bot α) :
x y = min x y

def with_top  :
Type u_1Type u_1

Attach to a type.

Equations
@[instance]
meta def with_top.has_to_format {α : Type u_1} [has_to_format α] :

@[instance]
def with_top.has_coe_t {α : Type u} :

Equations
@[instance]
def with_top.has_top {α : Type u} :

Equations
@[instance]
def with_top.inhabited {α : Type u} :

Equations
theorem with_top.none_eq_top {α : Type u} :

theorem with_top.some_eq_coe {α : Type u} (a : α) :

def with_top.rec_top_coe {α : Type u} {C : with_top αSort u_1} (h₁ : C ) (h₂ : Π (a : α), C a) (n : with_top α) :
C n

Recursor for with_top using the preferred forms and ↑a.

Equations
theorem with_top.coe_eq_coe {α : Type u} {a b : α} :
a = b a = b

@[simp]
theorem with_top.top_ne_coe {α : Type u} {a : α} :

@[simp]
theorem with_top.coe_ne_top {α : Type u} {a : α} :

@[instance]
def with_top.has_lt {α : Type u} [has_lt α] :

Equations
@[instance]
def with_top.has_le {α : Type u} [has_le α] :

Equations
@[simp]
theorem with_top.some_lt_some {α : Type u} [has_lt α] {a b : α} :
some a < some b a < b

@[simp]
theorem with_top.some_le_some {α : Type u} [has_le α] {a b : α} :
some a some b a b

@[simp]
theorem with_top.le_none {α : Type u} [has_le α] {a : with_top α} :

@[simp]
theorem with_top.some_lt_none {α : Type u} [has_lt α] {a : α} :

@[instance]
def with_top.preorder {α : Type u} [preorder α] :

Equations
@[simp]
theorem with_top.coe_le_coe {α : Type u} [partial_order α] {a b : α} :
a b a b

theorem with_top.le_coe {α : Type u} [partial_order α] {a b : α} {o : option α} :
a o(o b a b)

theorem with_top.le_coe_iff {α : Type u} [partial_order α] (b : α) (x : with_top α) :
x b ∃ (a : α), x = a a b

theorem with_top.coe_le_iff {α : Type u} [partial_order α] (a : α) (x : with_top α) :
a x ∀ (b : α), x = ba b

theorem with_top.lt_iff_exists_coe {α : Type u} [partial_order α] (a b : with_top α) :
a < b ∃ (p : α), a = p p < b

theorem with_top.coe_lt_coe {α : Type u} [partial_order α] {a b : α} :
a < b a < b

theorem with_top.coe_lt_top {α : Type u} [partial_order α] (a : α) :

theorem with_top.not_top_le_coe {α : Type u} [partial_order α] (a : α) :

@[instance]

Equations
theorem with_top.coe_inf {α : Type u} [semilattice_inf α] (a b : α) :
(a b) = a b

@[instance]

Equations
theorem with_top.coe_sup {α : Type u} [semilattice_sup α] (a b : α) :
(a b) = a b

theorem with_top.sup_eq_max {α : Type u} [decidable_linear_order α] (x y : with_top α) :
x y = max x y

theorem with_top.inf_eq_min {α : Type u} [decidable_linear_order α] (x y : with_top α) :
x y = min x y

theorem with_top.lt_iff_exists_coe_btwn {α : Type u} [partial_order α] [densely_ordered α] [no_top_order α] {a b : with_top α} :
a < b ∃ (x : α), a < x x < b

def subtype.semilattice_sup {α : Type u} [semilattice_sup α] {P : α → Prop} :
(∀ ⦃x y : α⦄, P xP yP (x y))semilattice_sup {x // P x}

A subtype forms a -semilattice if preserves the property.

Equations
def subtype.semilattice_inf {α : Type u} [semilattice_inf α] {P : α → Prop} :
(∀ ⦃x y : α⦄, P xP yP (x y))semilattice_inf {x // P x}

A subtype forms a -semilattice if preserves the property.

Equations
def subtype.semilattice_sup_bot {α : Type u} [semilattice_sup_bot α] {P : α → Prop} :
P (∀ ⦃x y : α⦄, P xP yP (x y))semilattice_sup_bot {x // P x}

A subtype forms a --semilattice if and preserve the property.

Equations
def subtype.semilattice_inf_bot {α : Type u} [semilattice_inf_bot α] {P : α → Prop} :
P (∀ ⦃x y : α⦄, P xP yP (x y))semilattice_inf_bot {x // P x}

A subtype forms a --semilattice if and preserve the property.

Equations
def subtype.semilattice_inf_top {α : Type u} [semilattice_inf_top α] {P : α → Prop} :
P (∀ ⦃x y : α⦄, P xP yP (x y))semilattice_inf_top {x // P x}

A subtype forms a --semilattice if and preserve the property.

Equations
def subtype.lattice {α : Type u} [lattice α] {P : α → Prop} :
(∀ ⦃x y : α⦄, P xP yP (x y))(∀ ⦃x y : α⦄, P xP yP (x y))lattice {x // P x}

A subtype forms a lattice if and preserve the property.

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

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

Equations
@[instance]
def prod.has_top (α : Type u) (β : Type v) [has_top α] [has_top β] :
has_top × β)

Equations
@[instance]
def prod.has_bot (α : Type u) (β : Type v) [has_bot α] [has_bot β] :
has_bot × β)

Equations
@[instance]
def prod.order_top (α : Type u) (β : Type v) [order_top α] [order_top β] :
order_top × β)

Equations
@[instance]
def prod.order_bot (α : Type u) (β : Type v) [order_bot α] [order_bot β] :
order_bot × β)

Equations
@[instance]
def prod.bounded_lattice (α : Type u) (β : Type v) [bounded_lattice α] [bounded_lattice β] :

Equations
def disjoint {α : Type u} [semilattice_inf_bot α] :
α → α → Prop

Two elements of a lattice are disjoint if their inf is the bottom element. (This generalizes disjoint sets, viewed as members of the subset lattice.)

Equations
theorem disjoint.eq_bot {α : Type u} [semilattice_inf_bot α] {a b : α} :
disjoint a ba b =

theorem disjoint_iff {α : Type u} [semilattice_inf_bot α] {a b : α} :
disjoint a b a b =

theorem disjoint.comm {α : Type u} [semilattice_inf_bot α] {a b : α} :

theorem disjoint.symm {α : Type u} [semilattice_inf_bot α] ⦃a b : α⦄ :
disjoint a bdisjoint b a

@[simp]
theorem disjoint_bot_left {α : Type u} [semilattice_inf_bot α] {a : α} :

@[simp]
theorem disjoint_bot_right {α : Type u} [semilattice_inf_bot α] {a : α} :

theorem disjoint.mono {α : Type u} [semilattice_inf_bot α] {a b c d : α} :
a bc ddisjoint b ddisjoint a c

theorem disjoint.mono_left {α : Type u} [semilattice_inf_bot α] {a b c : α} :
a bdisjoint b cdisjoint a c

theorem disjoint.mono_right {α : Type u} [semilattice_inf_bot α] {a b c : α} :
b cdisjoint a cdisjoint a b

@[simp]
theorem disjoint_self {α : Type u} [semilattice_inf_bot α] {a : α} :

theorem disjoint.ne {α : Type u} [semilattice_inf_bot α] {a b : α} :
a disjoint a ba b

@[simp]
theorem disjoint_sup_left {α : Type u} [bounded_distrib_lattice α] {a b c : α} :

@[simp]
theorem disjoint_sup_right {α : Type u} [bounded_distrib_lattice α] {a b c : α} :

theorem disjoint.sup_left {α : Type u} [bounded_distrib_lattice α] {a b c : α} :
disjoint a cdisjoint b cdisjoint (a b) c

theorem disjoint.sup_right {α : Type u} [bounded_distrib_lattice α] {a b c : α} :
disjoint a bdisjoint a cdisjoint a (b c)

is_compl predicate

structure is_compl {α : Type u} [bounded_lattice α] :
α → α → Prop

Two elements x and y are complements of each other if x ⊔ y = ⊤ and x ⊓ y = ⊥.

theorem is_compl.disjoint {α : Type u} [bounded_lattice α] {x y : α} :
is_compl x ydisjoint x y

theorem is_compl.symm {α : Type u} [bounded_lattice α] {x y : α} :
is_compl x yis_compl y x

theorem is_compl.of_eq {α : Type u} [bounded_lattice α] {x y : α} :
x y = x y = is_compl x y

theorem is_compl.inf_eq_bot {α : Type u} [bounded_lattice α] {x y : α} :
is_compl x yx y =

theorem is_compl.sup_eq_top {α : Type u} [bounded_lattice α] {x y : α} :
is_compl x yx y =

theorem is_compl.to_order_dual {α : Type u} [bounded_lattice α] {x y : α} :
is_compl x yis_compl x y

theorem is_compl.le_left_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :
is_compl x y(z x disjoint z y)

theorem is_compl.le_right_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :
is_compl x y(z y disjoint z x)

theorem is_compl.left_le_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :
is_compl x y(x z z y)

theorem is_compl.right_le_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :
is_compl x y(y z z x)

theorem is_compl.antimono {α : Type u} [bounded_distrib_lattice α] {x y x' y' : α} :
is_compl x yis_compl x' y'x x'y' y

theorem is_compl.right_unique {α : Type u} [bounded_distrib_lattice α] {x y z : α} :
is_compl x yis_compl x zy = z

theorem is_compl.left_unique {α : Type u} [bounded_distrib_lattice α] {x y z : α} :
is_compl x zis_compl y zx = y

theorem is_compl.sup_inf {α : Type u} [bounded_distrib_lattice α] {x y x' y' : α} :
is_compl x yis_compl x' y'is_compl (x x') (y y')

theorem is_compl.inf_sup {α : Type u} [bounded_distrib_lattice α] {x y x' y' : α} :
is_compl x yis_compl x' y'is_compl (x x') (y y')

theorem is_compl.inf_left_eq_bot_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :
is_compl y z(x y = x z)

theorem is_compl.inf_right_eq_bot_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :
is_compl y z(x z = x y)

theorem is_compl.disjoint_left_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :
is_compl y z(disjoint x y x z)

theorem is_compl.disjoint_right_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :
is_compl y z(disjoint x z x y)

theorem is_compl_bot_top {α : Type u} [bounded_lattice α] :

theorem is_compl_top_bot {α : Type u} [bounded_lattice α] :