# mathlibdocumentation

order.bounded_lattice

# ⊤ and ⊥, bounded lattices and variants #

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 #

• `has_<top/bot> α`: Typeclasses to declare the `⊤`/`⊥` notation.
• `order_<top/bot> α`: Order with a top/bottom element.
• `with_<top/bot> α`: Equips `option α` with the order on `α` plus `none` as the top/bottom element.
• `semilattice_<sup/inf>_<top/bot>`: Semilattice with a join/meet and a top/bottom element (all four combinations). Typical examples include `ℕ`.
• `bounded_lattice α`: Lattice with a top and bottom element.
• `bounded_distrib_lattice α`: Bounded and distributive lattice. Typical examples include `Prop` and `set α`.
• `is_compl x y`: In a bounded lattice, predicate for "`x` is a complement of `y`". Note that in a non distributive lattice, an element can have several complements.
• `is_complemented α`: Typeclass stating that any element of a lattice has a complement.

### Top, bottom element #

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

Typeclass for the `⊤` (`\top`) notation

Instances
@[class]
structure has_bot (α : Type u) :
Type u
• bot : α

Typeclass for the `⊥` (`\bot`) notation

Instances
@[instance]
def has_top_nonempty (α : Type u) [has_top α] :
@[instance]
def has_bot_nonempty (α : Type u) [has_bot α] :
@[class]
structure order_top (α : Type u) :
Type 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 greatest 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) [self : order_top α] :
@[instance]
def order_top.to_has_top (α : Type u) [self : order_top α] :
@[simp]
theorem le_top {α : Type u} [order_top α] {a : α} :
theorem top_unique {α : Type u} [order_top α] {a : α} (h : a) :
a =
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 : α} (h : a b) (h₂ : a = ) :
b =
theorem lt_top_iff_ne_top {α : Type u} [order_top α] {a : α} :
theorem ne_top_of_lt {α : Type u} [order_top α] {a b : α} (h : a < b) :
theorem ne_top_of_le_ne_top {α : Type u} [order_top α] {a b : α} (hb : b ) (hab : a b) :
theorem eq_top_of_maximal {α : Type u} [order_top α] {a : α} (h : ∀ (b : α), ¬a < b) :
a =
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 α} (H : ∀ (x y : α), x y x y) :
theorem order_top.ext {α : Type u_1} {A B : order_top α} (H : ∀ (x y : α), x y x y) :
A = B
@[class]
structure order_bot (α : Type u) :
Type 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 least 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) [self : order_bot α] :
@[instance]
def order_bot.to_has_bot (α : Type u) [self : order_bot α] :
@[simp]
theorem bot_le {α : Type u} [order_bot α] {a : α} :
theorem bot_unique {α : Type u} [order_bot α] {a : α} (h : 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 : α} (hb : b ) (hab : b a) :
theorem eq_bot_mono {α : Type u} [order_bot α] {a b : α} (h : a b) (h₂ : b = ) :
a =
theorem bot_lt_iff_ne_bot {α : Type u} [order_bot α] {a : α} :
theorem ne_bot_of_gt {α : Type u} [order_bot α] {a b : α} (h : a < b) :
theorem eq_bot_of_minimal {α : Type u} [order_bot α] {a : α} (h : ∀ (b : α), ¬b < a) :
a =
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 α} (H : ∀ (x y : α), x y x y) :
theorem order_bot.ext {α : Type u_1} {A B : order_bot α} (H : ∀ (x y : α), x y x y) :
A = B
@[class]
structure semilattice_sup_top (α : Type u) :
Type 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]
def semilattice_sup_top.to_order_top (α : Type u) [self : semilattice_sup_top α] :
@[instance]
@[simp]
theorem top_sup_eq {α : Type u} {a : α} :
@[simp]
theorem sup_top_eq {α : Type u} {a : α} :
@[instance]
def semilattice_sup_bot.to_order_bot (α : Type u) [self : semilattice_sup_bot α] :
@[instance]
@[class]
structure semilattice_sup_bot (α : Type u) :
Type 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} {a : α} :
a = a
@[simp]
theorem sup_bot_eq {α : Type u} {a : α} :
a = a
@[simp]
theorem sup_eq_bot_iff {α : Type u} {a b : α} :
a b = a = b =
@[instance]
Equations
@[class]
structure semilattice_inf_top (α : Type u) :
Type 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]
def semilattice_inf_top.to_order_top (α : Type u) [self : semilattice_inf_top α] :
@[instance]
@[simp]
theorem top_inf_eq {α : Type u} {a : α} :
a = a
@[simp]
theorem inf_top_eq {α : Type u} {a : α} :
a = a
@[simp]
theorem inf_eq_top_iff {α : Type u} {a b : α} :
a b = a = b =
@[instance]
def semilattice_inf_bot.to_order_bot (α : Type u) [self : semilattice_inf_bot α] :
@[class]
structure semilattice_inf_bot (α : Type u) :
Type 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
@[instance]
@[simp]
theorem bot_inf_eq {α : Type u} {a : α} :
@[simp]
theorem inf_bot_eq {α : Type u} {a : α} :

### Bounded lattice #

@[instance]
def bounded_lattice.to_order_top (α : Type u) [self : bounded_lattice α] :
@[instance]
def bounded_lattice.to_order_bot (α : Type u) [self : bounded_lattice α] :
@[instance]
def bounded_lattice.to_lattice (α : Type u) [self : bounded_lattice α] :
@[class]
structure bounded_lattice (α : Type u) :
Type 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
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
Equations
theorem bounded_lattice.ext {α : Type u_1} {A B : bounded_lattice α} (H : ∀ (x y : α), x y x y) :
A = B
@[instance]
@[class]
structure bounded_distrib_lattice (α : Type u_1) :
Type 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
@[instance]
theorem inf_eq_bot_iff_le_compl {α : Type u} {a b c : α} (h₁ : b c = ) (h₂ : b c = ) :
a b = a c
@[instance]

Propositions form a bounded distributive lattice.

Equations
@[instance]
Equations
@[simp]
theorem le_Prop_eq  :
has_le.le = λ (_x _y : Prop), _x → _y
@[simp]
theorem sup_Prop_eq  :
@[simp]
theorem inf_Prop_eq  :
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)
@[instance]
def pi.order_bot {α : Type u_1} {β : α → Type u_2} [Π (a : α), order_bot (β a)] :
order_bot (Π (a : α), β a)
Equations

### Function lattices #

@[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 : ι) :
@[instance]
def pi.semilattice_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup (α i)] :
semilattice_sup (Π (i : ι), α i)
Equations
@[instance]
def pi.semilattice_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf (α i)] :
semilattice_inf (Π (i : ι), α i)
Equations
@[instance]
def pi.semilattice_inf_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_bot (α i)] :
semilattice_inf_bot (Π (i : ι), α i)
Equations
@[instance]
def pi.semilattice_inf_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_top (α i)] :
semilattice_inf_top (Π (i : ι), α i)
Equations
@[instance]
def pi.semilattice_sup_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_bot (α i)] :
semilattice_sup_bot (Π (i : ι), α i)
Equations
@[instance]
def pi.semilattice_sup_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_top (α i)] :
semilattice_sup_top (Π (i : ι), α i)
Equations
@[instance]
def pi.lattice {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), lattice (α i)] :
lattice (Π (i : ι), α i)
Equations
@[instance]
def pi.bounded_lattice {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] :
bounded_lattice (Π (i : ι), α i)
Equations
theorem eq_bot_of_bot_eq_top {α : Type u_1} (hα : = ) (x : α) :
x =
theorem eq_top_of_bot_eq_top {α : Type u_1} (hα : = ) (x : α) :
x =
theorem subsingleton_of_top_le_bot {α : Type u_1} (h : ) :
theorem subsingleton_of_bot_eq_top {α : Type u_1} (hα : = ) :
theorem subsingleton_iff_bot_eq_top {α : Type u_1}  :

### `with_bot`, `with_top`#

def with_bot (α : Type u_1) :
Type u_1

Attach `⊥` to a type.

Equations
@[instance]
meta def with_bot.has_to_format {α : Type u_1}  :
@[instance]
def with_bot.has_coe_t {α : Type u} :
(with_bot α)
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 : 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
• h₂ = option.rec h₁ h₂
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.can_lift {α : Type u} :
Equations
@[instance]
def with_bot.preorder {α : Type u} [preorder α] :
Equations
@[instance]
def with_bot.partial_order {α : Type u}  :
Equations
@[instance]
def with_bot.order_bot {α : Type u}  :
Equations
@[simp]
theorem with_bot.coe_le_coe {α : Type u} [preorder α] {a b : α} :
a b a b
@[simp]
theorem with_bot.some_le_some {α : Type u} [preorder α] {a b : α} :
some a some b a b
theorem with_bot.coe_le {α : Type u} {a b : α} {o : option α} :
b o(a o a b)
theorem with_bot.coe_lt_coe {α : Type u} {a b : α} :
a < b a < b
theorem with_bot.le_coe_get_or_else {α : Type u} [preorder α] (a : with_bot α) (b : α) :
a b)
@[simp]
theorem with_bot.get_or_else_bot {α : Type u} (a : α) :
theorem with_bot.get_or_else_bot_le_iff {α : Type u} [order_bot α] {a : with_bot α} {b : α} :
a b
@[instance]
def with_bot.decidable_le {α : Type u} [preorder α]  :
Equations
@[instance]
def with_bot.decidable_lt {α : Type u} [has_lt α]  :
Equations
@[instance]
def with_bot.has_le.le.is_total {α : Type u}  :
@[instance]
def with_bot.linear_order {α : Type u} [linear_order α] :
Equations
@[instance]
def with_bot.semilattice_sup {α : Type u}  :
Equations
theorem with_bot.coe_sup {α : Type u} (a b : α) :
(a b) = a b
@[instance]
def with_bot.semilattice_inf {α : Type u}  :
Equations
theorem with_bot.coe_inf {α : Type u} (a b : α) :
(a b) = a b
@[instance]
def with_bot.lattice {α : Type u} [lattice α] :
Equations
theorem with_bot.lattice_eq_DLO {α : Type u} [linear_order α] :
theorem with_bot.sup_eq_max {α : Type u} [linear_order α] (x y : with_bot α) :
x y = max x y
theorem with_bot.inf_eq_min {α : Type u} [linear_order α] (x y : with_bot α) :
x y = min x y
theorem with_bot.coe_min {α : Type u} [linear_order α] (x y : α) :
(min x y) = min x y
theorem with_bot.coe_max {α : Type u} [linear_order α] (x y : α) :
(max x y) = max x y
@[instance]
def with_bot.order_top {α : Type u} [order_top α] :
Equations
@[instance]
def with_bot.bounded_lattice {α : Type u}  :
Equations
theorem with_bot.well_founded_lt {α : Type u}  :
@[instance]
def with_bot.densely_ordered {α : Type u} [no_bot_order α] :
def with_top (α : Type u_1) :
Type u_1

Attach `⊤` to a type.

Equations
@[instance]
meta def with_top.has_to_format {α : Type u_1}  :
@[instance]
def with_top.has_coe_t {α : Type u} :
(with_top α)
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 : 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
• h₂ = option.rec h₁ h₂
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.can_lift {α : Type u} :
Equations
@[instance]
def with_top.preorder {α : Type u} [preorder α] :
Equations
@[instance]
def with_top.partial_order {α : Type u}  :
Equations
@[instance]
def with_top.order_top {α : Type u}  :
Equations
@[simp]
theorem with_top.coe_le_coe {α : Type u} {a b : α} :
a b a b
theorem with_top.le_coe {α : Type u} {a b : α} {o : option α} :
a o(o b a b)
theorem with_top.le_coe_iff {α : Type u} {b : α} {x : with_top α} :
x b ∃ (a : α), x = a a b
theorem with_top.coe_le_iff {α : Type u} {a : α} {x : with_top α} :
a x ∀ (b : α), x = ba b
theorem with_top.lt_iff_exists_coe {α : Type u} {a b : with_top α} :
a < b ∃ (p : α), a = p p < b
theorem with_top.coe_lt_coe {α : Type u} {a b : α} :
a < b a < b
theorem with_top.coe_lt_top {α : Type u} (a : α) :
theorem with_top.coe_lt_iff {α : Type u} {a : α} {x : with_top α} :
a < x ∀ (b : α), x = ba < b
theorem with_top.not_top_le_coe {α : Type u} (a : α) :
@[instance]
def with_top.decidable_le {α : Type u} [preorder α]  :
Equations
@[instance]
def with_top.decidable_lt {α : Type u} [has_lt α]  :
Equations
@[instance]
def with_top.has_le.le.is_total {α : Type u}  :
@[instance]
def with_top.linear_order {α : Type u} [linear_order α] :
Equations
@[instance]
def with_top.semilattice_inf {α : Type u}  :
Equations
theorem with_top.coe_inf {α : Type u} (a b : α) :
(a b) = a b
@[instance]
def with_top.semilattice_sup {α : Type u}  :
Equations
theorem with_top.coe_sup {α : Type u} (a b : α) :
(a b) = a b
@[instance]
def with_top.lattice {α : Type u} [lattice α] :
Equations
theorem with_top.lattice_eq_DLO {α : Type u} [linear_order α] :
theorem with_top.sup_eq_max {α : Type u} [linear_order α] (x y : with_top α) :
x y = max x y
theorem with_top.inf_eq_min {α : Type u} [linear_order α] (x y : with_top α) :
x y = min x y
@[simp]
theorem with_top.coe_min {α : Type u} [linear_order α] (x y : α) :
(min x y) = min x y
@[simp]
theorem with_top.coe_max {α : Type u} [linear_order α] (x y : α) :
(max x y) = max x y
@[instance]
def with_top.order_bot {α : Type u} [order_bot α] :
Equations
@[instance]
def with_top.bounded_lattice {α : Type u}  :
Equations
theorem with_top.well_founded_lt {α : Type u_1}  :
@[instance]
def with_top.densely_ordered {α : Type u} [no_top_order α] :
theorem with_top.lt_iff_exists_coe_btwn {α : Type u} [no_top_order α] {a b : with_top α} :
a < b ∃ (x : α), a < x x < b

### Subtype, order dual, product lattices #

def subtype.semilattice_sup_bot {α : Type u} {P : α → Prop} (Pbot : P ) (Psup : ∀ ⦃x y : α⦄, P xP yP (x y)) :

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

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

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

Equations
def subtype.semilattice_sup_top {α : Type u} {P : α → Prop} (Ptop : P ) (Psup : ∀ ⦃x y : α⦄, P xP yP (x y)) :

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

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

A subtype forms a `⊓`-`⊤`-semilattice 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 order_dual.order_top (α : Type u) [order_bot α] :
Equations
@[instance]
def order_dual.order_bot (α : Type u) [order_top α] :
Equations
@[instance]
def order_dual.semilattice_sup_top (α : Type u)  :
Equations
@[instance]
def order_dual.semilattice_sup_bot (α : Type u)  :
Equations
@[instance]
def order_dual.semilattice_inf_top (α : Type u)  :
Equations
@[instance]
def order_dual.semilattice_inf_bot (α : Type u)  :
Equations
@[instance]
def order_dual.bounded_lattice (α : Type u)  :
Equations
@[instance]
def order_dual.bounded_distrib_lattice (α : Type u)  :
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.semilattice_sup_top (α : Type u) (β : Type v)  :
Equations
@[instance]
def prod.semilattice_inf_top (α : Type u) (β : Type v)  :
Equations
@[instance]
def prod.semilattice_sup_bot (α : Type u) (β : Type v)  :
Equations
@[instance]
def prod.semilattice_inf_bot (α : Type u) (β : Type v)  :
Equations
@[instance]
def prod.bounded_lattice (α : Type u) (β : Type v)  :
Equations
@[instance]
def prod.bounded_distrib_lattice (α : Type u) (β : Type v)  :
Equations

### Disjointness and complements #

def disjoint {α : Type u} (a b : α) :
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} {a b : α} (h : b) :
a b =
theorem disjoint_iff {α : Type u} {a b : α} :
b a b =
theorem disjoint.comm {α : Type u} {a b : α} :
b a
theorem disjoint.symm {α : Type u} ⦃a b : α⦄ :
b a
@[simp]
theorem disjoint_bot_left {α : Type u} {a : α} :
@[simp]
theorem disjoint_bot_right {α : Type u} {a : α} :
theorem disjoint.mono {α : Type u} {a b c d : α} (h₁ : a b) (h₂ : c d) :
d c
theorem disjoint.mono_left {α : Type u} {a b c : α} (h : a b) :
c c
theorem disjoint.mono_right {α : Type u} {a b c : α} (h : b c) :
c b
@[simp]
theorem disjoint_self {α : Type u} {a : α} :
a a =
theorem disjoint.ne {α : Type u} {a b : α} (ha : a ) (hab : b) :
a b
theorem disjoint.eq_bot_of_le {α : Type u} {a b : α} (hab : b) (h : a b) :
a =
theorem disjoint.of_disjoint_inf_of_le {α : Type u} {a b c : α} (h : disjoint (a b) c) (hle : a c) :
b
theorem disjoint.of_disjoint_inf_of_le' {α : Type u} {a b c : α} (h : disjoint (a b) c) (hle : b c) :
b
@[simp]
theorem disjoint_top {α : Type u} {a : α} :
a =
@[simp]
theorem top_disjoint {α : Type u} {a : α} :
a =
theorem eq_bot_of_disjoint_absorbs {α : Type u} {a b : α} (w : b) (h : a b = a) :
b =
@[simp]
theorem disjoint_sup_left {α : Type u} {a b c : α} :
disjoint (a b) c c c
@[simp]
theorem disjoint_sup_right {α : Type u} {a b c : α} :
(b c) b c
theorem disjoint.sup_left {α : Type u} {a b c : α} (ha : c) (hb : c) :
disjoint (a b) c
theorem disjoint.sup_right {α : Type u} {a b c : α} (hb : b) (hc : c) :
(b c)
theorem disjoint.left_le_of_le_sup_right {α : Type u} {a b c : α} (h : a b c) (hd : c) :
a b
theorem disjoint.left_le_of_le_sup_left {α : Type u} {a b c : α} (h : a c b) (hd : c) :
a b
structure is_compl {α : Type u} (x y : α) :
Prop

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

theorem is_compl.disjoint {α : Type u} {x y : α} (h : y) :
y
theorem is_compl.symm {α : Type u} {x y : α} (h : y) :
x
theorem is_compl.of_eq {α : Type u} {x y : α} (h₁ : x y = ) (h₂ : x y = ) :
y
theorem is_compl.inf_eq_bot {α : Type u} {x y : α} (h : y) :
x y =
theorem is_compl.sup_eq_top {α : Type u} {x y : α} (h : y) :
x y =
theorem is_compl.to_order_dual {α : Type u} {x y : α} (h : y) :
y
theorem is_compl.inf_left_eq_bot_iff {α : Type u} {x y z : α} (h : z) :
x y = x z
theorem is_compl.inf_right_eq_bot_iff {α : Type u} {x y z : α} (h : z) :
x z = x y
theorem is_compl.disjoint_left_iff {α : Type u} {x y z : α} (h : z) :
y x z
theorem is_compl.disjoint_right_iff {α : Type u} {x y z : α} (h : z) :
z x y
theorem is_compl.le_left_iff {α : Type u} {x y z : α} (h : y) :
z x y
theorem is_compl.le_right_iff {α : Type u} {x y z : α} (h : y) :
z y x
theorem is_compl.left_le_iff {α : Type u} {x y z : α} (h : y) :
x z z y
theorem is_compl.right_le_iff {α : Type u} {x y z : α} (h : y) :
y z z x
theorem is_compl.antimono {α : Type u} {x y x' y' : α} (h : y) (h' : is_compl x' y') (hx : x x') :
y' y
theorem is_compl.right_unique {α : Type u} {x y z : α} (hxy : y) (hxz : z) :
y = z
theorem is_compl.left_unique {α : Type u} {x y z : α} (hxz : z) (hyz : z) :
x = y
theorem is_compl.sup_inf {α : Type u} {x y x' y' : α} (h : y) (h' : is_compl x' y') :
is_compl (x x') (y y')
theorem is_compl.inf_sup {α : Type u} {x y x' y' : α} (h : y) (h' : is_compl x' y') :
is_compl (x x') (y y')
theorem is_compl_bot_top {α : Type u}  :
theorem is_compl_top_bot {α : Type u}  :
theorem eq_top_of_is_compl_bot {α : Type u} {x : α} (h : ) :
x =
theorem eq_top_of_bot_is_compl {α : Type u} {x : α} (h : x) :
x =
theorem eq_bot_of_is_compl_top {α : Type u} {x : α} (h : ) :
x =
theorem eq_bot_of_top_is_compl {α : Type u} {x : α} (h : x) :
x =
@[class]
structure is_complemented (α : Type u_1)  :
Prop
• exists_is_compl : ∀ (a : α), ∃ (b : α), b

A complemented bounded lattice is one where every element has a (not necessarily unique) complement.

Instances
@[instance]
theorem bot_ne_top {α : Type u} [nontrivial α] :
theorem top_ne_bot {α : Type u} [nontrivial α] :
@[instance]
Equations
@[simp]
theorem top_eq_tt  :
@[simp]
theorem bot_eq_ff  :