# mathlibdocumentation

order.bounded_order

# ⊤ 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.
• `bounded_order α`: Order with a top and bottom element.
• `with_<top/bot> α`: Equips `option α` with the order on `α` plus `none` as the top/bottom element.
• `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.
• `complemented_lattice α`: Typeclass stating that any element of a lattice has a complement.

## Common lattices #

• Distributive lattices with a bottom element. Notated by `[distrib_lattice α] [order_bot α]` It captures the properties of `disjoint` that are common to `generalized_boolean_algebra` and `distrib_lattice` when `order_bot`.
• Bounded and distributive lattice. Notated by `[distrib_lattice α] [bounded_order α]`. Typical examples include `Prop` and `set α`.

### Top, bottom element #

@[class]
structure has_top (α : Type u) :
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) :
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 α] :
Type u
• top : α
• le_top : ∀ (a : α), a

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} [order_top α] {a : α} :
a =
@[simp]
theorem is_top_iff_eq_top {α : Type u} [order_top α] {a : α} :
a =
theorem not_is_max_iff_ne_top {α : Type u} [order_top α] {a : α} :
theorem not_is_top_iff_ne_top {α : Type u} [order_top α] {a : α} :
theorem is_max.eq_top {α : Type u} [order_top α] {a : α} :
a =

Alias of the forward direction of `is_max_iff_eq_top`.

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

Alias of the forward direction of `is_top_iff_eq_top`.

@[simp]
theorem top_le_iff {α : 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 : α} :
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 : α} :
@[simp]
theorem not_lt_top_iff {α : Type u} [order_top α] {a : α} :
theorem eq_top_or_lt_top {α : Type u} [order_top α] (a : α) :
a = a <
theorem ne.lt_top {α : Type u} [order_top α] {a : α} (h : a ) :
a <
theorem ne.lt_top' {α : Type u} [order_top α] {a : α} (h : a) :
a <
theorem ne_top_of_le_ne_top {α : Type u} [order_top α] {a b : α} (hb : b ) (hab : a b) :
theorem strict_mono.apply_eq_top_iff {α : Type u} {β : Type v} [order_top α] [preorder β] {f : α → β} {a : α} (hf : strict_mono f) :
f a = f a =
theorem strict_anti.apply_eq_top_iff {α : Type u} {β : Type v} [order_top α] [preorder β] {f : α → β} {a : α} (hf : strict_anti f) :
f a = f a =
theorem not_is_min_top {α : Type u} [order_top α] [nontrivial α] :
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} {A B : order_top α} :
A = B
@[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
@[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]
def order_dual.order_top (α : Type u) [has_le α] [order_bot α] :
Equations
@[protected, instance]
def order_dual.order_bot (α : Type u) [has_le α] [order_top α] :
Equations
@[simp]
theorem order_dual.of_dual_bot (α : Type u) [has_top α] :
@[simp]
theorem order_dual.of_dual_top (α : Type u) [has_bot α] :
@[simp]
theorem order_dual.to_dual_bot (α : Type u) [has_bot α] :
@[simp]
theorem order_dual.to_dual_top (α : Type u) [has_top α] :
@[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} [order_bot α] {a : α} :
a =
@[simp]
theorem is_bot_iff_eq_bot {α : Type u} [order_bot α] {a : α} :
a =
theorem not_is_min_iff_ne_bot {α : Type u} [order_bot α] {a : α} :
theorem not_is_bot_iff_ne_bot {α : Type u} [order_bot α] {a : α} :
theorem is_min.eq_bot {α : Type u} [order_bot α] {a : α} :
a =

Alias of the forward direction of `is_min_iff_eq_bot`.

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

Alias of the forward direction of `is_bot_iff_eq_bot`.

@[simp]
theorem le_bot_iff {α : 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 : α} :
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 : α} :
@[simp]
theorem not_bot_lt_iff {α : Type u} [order_bot α] {a : α} :
theorem eq_bot_or_bot_lt {α : Type u} [order_bot α] (a : α) :
a = < a
theorem eq_bot_of_minimal {α : Type u} [order_bot α] {a : α} (h : ∀ (b : α), ¬b < a) :
a =
theorem ne.bot_lt {α : Type u} [order_bot α] {a : α} (h : a ) :
< a
theorem ne.bot_lt' {α : Type u} [order_bot α] {a : α} (h : a) :
< a
theorem ne_bot_of_le_ne_bot {α : Type u} [order_bot α] {a b : α} (hb : b ) (hab : b a) :
theorem strict_mono.apply_eq_bot_iff {α : Type u} {β : Type v} [order_bot α] [preorder β] {f : α → β} {a : α} (hf : strict_mono f) :
f a = f a =
theorem strict_anti.apply_eq_bot_iff {α : Type u} {β : Type v} [order_bot α] [preorder β] {f : α → β} {a : α} (hf : strict_anti f) :
f a = f a =
theorem not_is_max_bot {α : Type u} [order_bot α] [nontrivial α] :
theorem strict_mono.minimal_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} {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} {A B : order_bot α} :
A = B
@[simp]
theorem top_sup_eq {α : Type u} [order_top α] {a : α} :
@[simp]
theorem sup_top_eq {α : Type u} [order_top α] {a : α} :
@[simp]
theorem bot_sup_eq {α : Type u} [order_bot α] {a : α} :
a = a
@[simp]
theorem sup_bot_eq {α : Type u} [order_bot α] {a : α} :
a = a
@[simp]
theorem sup_eq_bot_iff {α : Type u} [order_bot α] {a b : α} :
a b = a = b =
@[simp]
theorem top_inf_eq {α : Type u} [order_top α] {a : α} :
a = a
@[simp]
theorem inf_top_eq {α : Type u} [order_top α] {a : α} :
a = a
@[simp]
theorem inf_eq_top_iff {α : Type u} [order_top α] {a b : α} :
a b = a = b =
@[simp]
theorem bot_inf_eq {α : Type u} [order_bot α] {a : α} :
@[simp]
theorem inf_bot_eq {α : Type u} [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 α] :
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
@[protected, instance]
def order_dual.bounded_order (α : Type u) [has_le α]  :
Equations
theorem bounded_order.ext {α : Type u_1} {A B : bounded_order α} :
A = B
@[protected, instance]

Propositions form a distributive lattice.

Equations
@[protected, instance]

Propositions form a bounded order.

Equations
@[protected, instance]
@[protected, instance]
noncomputable def Prop.linear_order  :
Equations
@[simp]
theorem sup_Prop_eq  :
@[simp]
theorem inf_Prop_eq  :

#### 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 smonotone (P x)) :
monotone (λ (y : α), ∀ (x : β), x sP x y)
theorem antitone.ball {α : Type u} {β : Type v} [preorder α] {P : β → α → Prop} {s : set β} (hP : ∀ (x : β), x santitone (P x)) :
antitone (λ (y : α), ∀ (x : β), x sP x y)
theorem exists_ge_and_iff_exists {α : Type u} {P : α → Prop} {x₀ : α} (hP : monotone P) :
(∃ (x : α), x₀ x P x) ∃ (x : α), P x
theorem exists_le_and_iff_exists {α : Type u} {P : α → Prop} {x₀ : α} (hP : antitone P) :
(∃ (x : α), x x₀ P x) ∃ (x : α), P x

### Function lattices #

@[protected, instance]
def pi.has_bot {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_bot (α' i)] :
has_bot (Π (i : ι), α' i)
Equations
@[simp]
theorem pi.bot_apply {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_bot (α' i)] (i : ι) :
theorem pi.bot_def {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_bot (α' i)] :
= λ (i : ι),
@[protected, instance]
def pi.has_top {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_top (α' i)] :
has_top (Π (i : ι), α' i)
Equations
@[simp]
theorem pi.top_apply {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_top (α' i)] (i : ι) :
theorem pi.top_def {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_top (α' i)] :
= λ (i : ι),
@[protected, instance]
def pi.order_top {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_le (α' i)] [Π (i : ι), order_top (α' i)] :
order_top (Π (i : ι), α' i)
Equations
@[protected, instance]
def pi.order_bot {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_le (α' i)] [Π (i : ι), order_bot (α' i)] :
order_bot (Π (i : ι), α' i)
Equations
@[protected, instance]
def pi.bounded_order {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_le (α' i)] [Π (i : ι), bounded_order (α' i)] :
bounded_order (Π (i : ι), α' i)
Equations
theorem eq_bot_of_bot_eq_top {α : Type u} (hα : = ) (x : α) :
x =
theorem eq_top_of_bot_eq_top {α : Type u} (hα : = ) (x : α) :
x =
theorem subsingleton_of_top_le_bot {α : Type u} (h : ) :
theorem subsingleton_of_bot_eq_top {α : Type u} (hα : = ) :
theorem subsingleton_iff_bot_eq_top {α : Type u}  :
@[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 ba 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 ba 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 β] (f : α → β) (map_le : ∀ (a b : α), f a f ba b) (map_top : f = ) (map_bot : f = ) :

Pullback a `bounded_order`.

Equations

### `with_bot`, `with_top`#

def with_bot (α : Type u_1) :
Type u_1

Attach `⊥` to a type.

Equations
Instances for `with_bot`
@[protected, instance]
meta def with_bot.has_to_format {α : Type u}  :
@[protected, instance]
def with_bot.has_repr {α : Type u} [has_repr α] :
Equations
@[protected, instance]
def with_bot.has_coe_t {α : Type u} :
(with_bot α)
Equations
@[protected, instance]
def with_bot.has_bot {α : Type u} :
Equations
@[protected, instance]
meta def with_bot.has_reflect {α : Type} [reflected Type α] [has_reflect α] :
@[protected, 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 : α) :
@[simp]
theorem with_bot.bot_ne_coe {α : Type u} {a : α} :
@[simp]
theorem with_bot.coe_ne_bot {α : 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₂
@[simp]
theorem with_bot.rec_bot_coe_bot {α : Type u} {C : Sort u_1} (d : C ) (f : Π (a : α), C a) :
= d
@[simp]
theorem with_bot.rec_bot_coe_coe {α : Type u} {C : Sort u_1} (d : C ) (f : Π (a : α), C a) (x : α) :
= f x
def with_bot.unbot' {α : Type u} (d : α) (x : with_bot α) :
α

Specialization of `option.get_or_else` to values in `with_bot α` that respects API boundaries.

Equations
@[simp]
theorem with_bot.unbot'_bot {α : Type u_1} (d : α) :
@[simp]
theorem with_bot.unbot'_coe {α : Type u_1} (d x : α) :
= x
@[norm_cast]
theorem with_bot.coe_eq_coe {α : Type u} {a b : α} :
a = b a = b
def with_bot.map {α : Type u} {β : Type v} (f : α → β) :

Lift a map `f : α → β` to `with_bot α → with_bot β`. Implemented using `option.map`.

Equations
@[simp]
theorem with_bot.map_bot {α : Type u} {β : Type v} (f : α → β) :
@[simp]
theorem with_bot.map_coe {α : Type u} {β : Type v} (f : α → β) (a : α) :
= (f a)
theorem with_bot.ne_bot_iff_exists {α : Type u} {x : with_bot α} :
x ∃ (a : α), a = x
def with_bot.unbot {α : Type u} (x : with_bot α) :
x → α

Deconstruct a `x : with_bot α` to the underlying value in `α`, given a proof that `x ≠ ⊥`.

Equations
@[simp]
theorem with_bot.coe_unbot {α : Type u} (x : with_bot α) (h : x ) :
(x.unbot h) = x
@[simp]
theorem with_bot.unbot_coe {α : Type u} (x : α) (h : x := with_bot.coe_ne_bot) :
x.unbot h = x
@[protected, instance]
def with_bot.can_lift {α : Type u} :
Equations
@[protected, instance]
def with_bot.has_le {α : Type u} [has_le α] :
Equations
@[simp]
theorem with_bot.some_le_some {α : Type u} {a b : α} [has_le α] :
a b
@[simp, norm_cast]
theorem with_bot.coe_le_coe {α : Type u} {a b : α} [has_le α] :
a b a b
@[simp]
theorem with_bot.none_le {α : Type u} [has_le α] {a : with_bot α} :
@[protected, instance]
def with_bot.order_bot {α : Type u} [has_le α] :
Equations
@[protected, instance]
def with_bot.order_top {α : Type u} [has_le α] [order_top α] :
Equations
@[protected, instance]
def with_bot.bounded_order {α : Type u} [has_le α] [order_top α] :
Equations
theorem with_bot.not_coe_le_bot {α : Type u} [has_le α] (a : α) :
theorem with_bot.coe_le {α : Type u} {a b : α} [has_le α] {o : option α} :
b o(a o a b)
theorem with_bot.coe_le_iff {α : Type u} {a : α} [has_le α] {x : with_bot α} :
a x ∃ (b : α), x = b a b
theorem with_bot.le_coe_iff {α : Type u} {b : α} [has_le α] {x : with_bot α} :
x b ∀ (a : α), x = aa b
@[protected]
theorem is_max.with_bot {α : Type u} {a : α} [has_le α] (h : is_max a) :
@[protected, instance]
def with_bot.has_lt {α : Type u} [has_lt α] :
Equations
@[simp]
theorem with_bot.some_lt_some {α : Type u} {a b : α} [has_lt α] :
a < b
@[simp, norm_cast]
theorem with_bot.coe_lt_coe {α : Type u} {a b : α} [has_lt α] :
a < b a < b
@[simp]
theorem with_bot.none_lt_some {α : Type u} [has_lt α] (a : α) :
theorem with_bot.bot_lt_coe {α : Type u} [has_lt α] (a : α) :
@[simp]
theorem with_bot.not_lt_none {α : Type u} [has_lt α] (a : with_bot α) :
theorem with_bot.lt_iff_exists_coe {α : Type u} [has_lt α] {a b : with_bot α} :
a < b ∃ (p : α), b = p a < p
theorem with_bot.lt_coe_iff {α : Type u} {b : α} [has_lt α] {x : with_bot α} :
x < b ∀ (a : α), x = aa < b
@[protected, instance]
def with_bot.preorder {α : Type u} [preorder α] :
Equations
@[protected, instance]
def with_bot.partial_order {α : Type u}  :
Equations
theorem with_bot.map_le_iff {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α → β) (mono_iff : ∀ {a b : α}, f a f b a b) (a b : with_bot α) :
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} [has_le α] [order_bot α] {a : with_bot α} {b : α} :
a b
theorem with_bot.get_or_else_bot_lt_iff {α : Type u} [order_bot α] {a : with_bot α} {b : α} (ha : a ) :
a < b
@[protected, instance]
def with_bot.semilattice_sup {α : Type u}  :
Equations
theorem with_bot.coe_sup {α : Type u} (a b : α) :
(a b) = a b
@[protected, instance]
def with_bot.semilattice_inf {α : Type u}  :
Equations
theorem with_bot.coe_inf {α : Type u} (a b : α) :
(a b) = a b
@[protected, instance]
def with_bot.lattice {α : Type u} [lattice α] :
Equations
@[protected, instance]
def with_bot.decidable_le {α : Type u} [has_le α]  :
Equations
@[protected, instance]
def with_bot.decidable_lt {α : Type u} [has_lt α]  :
Equations
@[protected, instance]
def with_bot.is_total_le {α : Type u} [has_le α]  :
@[protected, instance]
def with_bot.linear_order {α : Type u} [linear_order α] :
Equations
@[norm_cast]
theorem with_bot.coe_min {α : Type u} [linear_order α] (x y : α) :
y) =
@[norm_cast]
theorem with_bot.coe_max {α : Type u} [linear_order α] (x y : α) :
y) =
theorem with_bot.well_founded_lt {α : Type u} [preorder α]  :
@[protected, instance]
def with_bot.densely_ordered {α : Type u} [has_lt α] [no_min_order α] :
theorem with_bot.lt_iff_exists_coe_btwn {α : Type u} [preorder α] [no_min_order α] {a b : with_bot α} :
a < b ∃ (x : α), a < x x < b
@[protected, instance]
def with_bot.no_top_order {α : Type u} [has_le α] [no_top_order α] [nonempty α] :
@[protected, instance]
def with_bot.no_max_order {α : Type u} [has_lt α] [no_max_order α] [nonempty α] :
def with_top (α : Type u_1) :
Type u_1

Attach `⊤` to a type.

Equations
Instances for `with_top`
@[protected, instance]
meta def with_top.has_to_format {α : Type u}  :
@[protected, instance]
def with_top.has_repr {α : Type u} [has_repr α] :
Equations
@[protected, instance]
def with_top.has_coe_t {α : Type u} :
(with_top α)
Equations
@[protected, instance]
def with_top.has_top {α : Type u} :
Equations
@[protected, instance]
meta def with_top.has_reflect {α : Type} [reflected Type α] [has_reflect α] :
@[protected, 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 : α) :
@[simp]
theorem with_top.top_ne_coe {α : Type u} {a : α} :
@[simp]
theorem with_top.coe_ne_top {α : 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₂
@[simp]
theorem with_top.rec_top_coe_top {α : Type u} {C : Sort u_1} (d : C ) (f : Π (a : α), C a) :
= d
@[simp]
theorem with_top.rec_top_coe_coe {α : Type u} {C : Sort u_1} (d : C ) (f : Π (a : α), C a) (x : α) :
= f x
@[protected]
def with_top.to_dual {α : Type u} :

`with_top.to_dual` is the equivalence sending `⊤` to `⊥` and any `a : α` to `to_dual a : αᵒᵈ`. See `with_top.to_dual_bot_equiv` for the related order-iso.

Equations
@[protected]
def with_top.of_dual {α : Type u} :

`with_top.of_dual` is the equivalence sending `⊤` to `⊥` and any `a : αᵒᵈ` to `of_dual a : α`. See `with_top.to_dual_bot_equiv` for the related order-iso.

Equations
@[protected]
def with_bot.to_dual {α : Type u} :

`with_bot.to_dual` is the equivalence sending `⊥` to `⊤` and any `a : α` to `to_dual a : αᵒᵈ`. See `with_bot.to_dual_top_equiv` for the related order-iso.

Equations
@[protected]
def with_bot.of_dual {α : Type u} :

`with_bot.of_dual` is the equivalence sending `⊥` to `⊤` and any `a : αᵒᵈ` to `of_dual a : α`. See `with_bot.to_dual_top_equiv` for the related order-iso.

Equations
@[simp]
theorem with_top.to_dual_symm_apply {α : Type u} (a : with_bot αᵒᵈ) :
@[simp]
theorem with_top.of_dual_symm_apply {α : Type u} (a : with_bot α) :
@[simp]
theorem with_top.to_dual_apply_top {α : Type u} :
@[simp]
theorem with_top.of_dual_apply_top {α : Type u} :
@[simp]
theorem with_top.to_dual_apply_coe {α : Type u} (a : α) :
@[simp]
theorem with_top.of_dual_apply_coe {α : Type u} (a : αᵒᵈ) :
def with_top.untop' {α : Type u} (d : α) (x : with_top α) :
α

Specialization of `option.get_or_else` to values in `with_top α` that respects API boundaries.

Equations
@[simp]
theorem with_top.untop'_top {α : Type u_1} (d : α) :
@[simp]
theorem with_top.untop'_coe {α : Type u_1} (d x : α) :
= x
@[norm_cast]
theorem with_top.coe_eq_coe {α : Type u} {a b : α} :
a = b a = b
def with_top.map {α : Type u} {β : Type v} (f : α → β) :

Lift a map `f : α → β` to `with_top α → with_top β`. Implemented using `option.map`.

Equations
@[simp]
theorem with_top.map_top {α : Type u} {β : Type v} (f : α → β) :
@[simp]
theorem with_top.map_coe {α : Type u} {β : Type v} (f : α → β) (a : α) :
= (f a)
theorem with_top.map_to_dual {α : Type u} {β : Type v} (f : αᵒᵈ → βᵒᵈ) (a : with_bot α) :
theorem with_top.map_of_dual {α : Type u} {β : Type v} (f : α → β) (a : with_bot αᵒᵈ) :
theorem with_top.to_dual_map {α : Type u} {β : Type v} (f : α → β) (a : with_top α) :
theorem with_top.of_dual_map {α : Type u} {β : Type v} (f : αᵒᵈ → βᵒᵈ) (a : with_top αᵒᵈ) :
theorem with_top.ne_top_iff_exists {α : Type u} {x : with_top α} :
x ∃ (a : α), a = x
def with_top.untop {α : Type u} (x : with_top α) :
x → α

Deconstruct a `x : with_top α` to the underlying value in `α`, given a proof that `x ≠ ⊤`.

Equations
@[simp]
theorem with_top.coe_untop {α : Type u} (x : with_top α) (h : x ) :
(x.untop h) = x
@[simp]
theorem with_top.untop_coe {α : Type u} (x : α) (h : x := with_top.coe_ne_top) :
x.untop h = x
@[protected, instance]
def with_top.can_lift {α : Type u} :
Equations
@[protected, instance]
def with_top.has_le {α : Type u} [has_le α] :
Equations
theorem with_top.to_dual_le_iff {α : Type u} [has_le α] {a : with_top α} {b : with_bot αᵒᵈ} :
theorem with_top.le_to_dual_iff {α : Type u} [has_le α] {a : with_bot αᵒᵈ} {b : with_top α} :
@[simp]
theorem with_top.to_dual_le_to_dual_iff {α : Type u} [has_le α] {a b : with_top α} :
b a
theorem with_top.of_dual_le_iff {α : Type u} [has_le α] {a : with_top αᵒᵈ} {b : with_bot α} :
theorem with_top.le_of_dual_iff {α : Type u} [has_le α] {a : with_bot α} {b : with_top αᵒᵈ} :
@[simp]
theorem with_top.of_dual_le_of_dual_iff {α : Type u} [has_le α] {a b : with_top αᵒᵈ} :
b a
@[simp, norm_cast]
theorem with_top.coe_le_coe {α : Type u} {a b : α} [has_le α] :
a b a b
@[simp]
theorem with_top.some_le_some {α : Type u} {a b : α} [has_le α] :
a b
@[simp]
theorem with_top.le_none {α : Type u} [has_le α] {a : with_top α} :
@[protected, instance]
def with_top.order_top {α : Type u} [has_le α] :
Equations
@[protected, instance]
def with_top.order_bot {α : Type u} [has_le α] [order_bot α] :
Equations
@[protected, instance]
def with_top.bounded_order {α : Type u} [has_le α] [order_bot α] :
Equations
theorem with_top.not_top_le_coe {α : Type u} [has_le α] (a : α) :
theorem with_top.le_coe {α : Type u} {a b : α} [has_le α] {o : option α} :
a o(o b a b)
theorem with_top.le_coe_iff {α : Type u} {b : α} [has_le α] {x : with_top α} :
x b ∃ (a : α), x = a a b
theorem with_top.coe_le_iff {α : Type u} {a : α} [has_le α] {x : with_top α} :
a x ∀ (b : α), x = ba b
@[protected]
theorem is_min.with_top {α : Type u} {a : α} [has_le α] (h : is_min a) :
@[protected, instance]
def with_top.has_lt {α : Type u} [has_lt α] :
Equations
theorem with_top.to_dual_lt_iff {α : Type u} [has_lt α] {a : with_top α} {b : with_bot αᵒᵈ} :
theorem with_top.lt_to_dual_iff {α : Type u} [has_lt α] {a : with_bot αᵒᵈ} {b : with_top α} :
@[simp]
theorem with_top.to_dual_lt_to_dual_iff {α : Type u} [has_lt α] {a b : with_top α} :
b < a
theorem with_top.of_dual_lt_iff {α : Type u} [has_lt α] {a : with_top αᵒᵈ} {b : with_bot α} :
theorem with_top.lt_of_dual_iff {α : Type u} [has_lt α] {a : with_bot α} {b : with_top αᵒᵈ} :
@[simp]
theorem with_top.of_dual_lt_of_dual_iff {α : Type u} [has_lt α] {a b : with_top αᵒᵈ} :
b < a
@[simp]
theorem with_bot.to_dual_symm_apply {α : Type u} (a : with_top αᵒᵈ) :
@[simp]
theorem with_bot.of_dual_symm_apply {α : Type u} (a : with_top α) :
@[simp]
theorem with_bot.to_dual_apply_bot {α : Type u} :
@[simp]
theorem with_bot.of_dual_apply_bot {α : Type u} :
@[simp]
theorem with_bot.to_dual_apply_coe {α : Type u} (a : α) :
@[simp]
theorem with_bot.of_dual_apply_coe {α : Type u} (a : αᵒᵈ) :
theorem with_bot.map_to_dual {α : Type u} {β : Type v} (f : αᵒᵈ → βᵒᵈ) (a : with_top α) :
theorem with_bot.map_of_dual {α : Type u} {β : Type v} (f : α → β) (a : with_top αᵒᵈ) :
theorem with_bot.to_dual_map {α : Type u} {β : Type v} (f : α → β) (a : with_bot α) :
theorem with_bot.of_dual_map {α : Type u} {β : Type v} (f : αᵒᵈ → βᵒᵈ) (a : with_bot αᵒᵈ) :
theorem with_bot.to_dual_le_iff {α : Type u} [has_le α] {a : with_bot α} {b : with_top αᵒᵈ} :
theorem with_bot.le_to_dual_iff {α : Type u} [has_le α] {a : with_top αᵒᵈ} {b : with_bot α} :
@[simp]
theorem with_bot.to_dual_le_to_dual_iff {α : Type u} [has_le α] {a b : with_bot α} :
b a
theorem with_bot.of_dual_le_iff {α : Type u} [has_le α] {a : with_bot αᵒᵈ} {b : with_top α} :
theorem with_bot.le_of_dual_iff {α : Type u} [has_le α] {a : with_top α} {b : with_bot αᵒᵈ} :
@[simp]
theorem with_bot.of_dual_le_of_dual_iff {α : Type u} [has_le α] {a b : with_bot αᵒᵈ} :
b a
theorem with_bot.to_dual_lt_iff {α : Type u} [has_lt α] {a : with_bot α} {b : with_top αᵒᵈ} :
theorem with_bot.lt_to_dual_iff {α : Type u} [has_lt α] {a : with_top αᵒᵈ} {b : with_bot α} :
@[simp]
theorem with_bot.to_dual_lt_to_dual_iff {α : Type u} [has_lt α] {a b : with_bot α} :
b < a
theorem with_bot.of_dual_lt_iff {α : Type u} [has_lt α] {a : with_bot αᵒᵈ} {b : with_top α} :
theorem with_bot.lt_of_dual_iff {α : Type u} [has_lt α] {a : with_top α} {b : with_bot αᵒᵈ} :
@[simp]
theorem with_bot.of_dual_lt_of_dual_iff {α : Type u} [has_lt α] {a b : with_bot αᵒᵈ} :
b < a
@[simp, norm_cast]
theorem with_top.coe_lt_coe {α : Type u} [has_lt α] {a b : α} :
a < b a < b
@[simp]
theorem with_top.some_lt_some {α : Type u} [has_lt α] {a b : α} :
a < b
theorem with_top.coe_lt_top {α : Type u} [has_lt α] (a : α) :
@[simp]
theorem with_top.some_lt_none {α : Type u} [has_lt α] (a : α) :
@[simp]
theorem with_top.not_none_lt {α : Type u} [has_lt α] (a : with_top α) :
theorem with_top.lt_iff_exists_coe {α : Type u} [has_lt α] {a b : with_top α} :
a < b ∃ (p : α), a = p p < b
theorem with_top.coe_lt_iff {α : Type u} [has_lt α] {a : α} {x : with_top α} :
a < x ∀ (b : α), x = ba < b
@[protected, instance]
def with_top.preorder {α : Type u} [preorder α] :
Equations
@[protected, instance]
def with_top.partial_order {α : Type u}  :
Equations
theorem with_top.map_le_iff {α : Type u} {β : Type v} [preorder α] [preorder β] (f : α → β) (a b : with_top α) (mono_iff : ∀ {a b : α}, f a f b a b) :
a b a b
@[protected, instance]
def with_top.semilattice_inf {α : Type u}  :
Equations
theorem with_top.coe_inf {α : Type u} (a b : α) :
(a b) = a b
@[protected, instance]
def with_top.semilattice_sup {α : Type u}  :
Equations
theorem with_top.coe_sup {α : Type u} (a b : α) :
(a b) = a b
@[protected, instance]
def with_top.lattice {α : Type u} [lattice α] :
Equations
@[protected, instance]
def with_top.decidable_le {α : Type u} [has_le α]  :
Equations
@[protected, instance]
def with_top.decidable_lt {α : Type u} [has_lt α]  :
Equations
@[protected, instance]
def with_top.is_total_le {α : Type u} [has_le α]  :
@[protected, instance]
def with_top.linear_order {α : Type u} [linear_order α] :
Equations
@[simp, norm_cast]
theorem with_top.coe_min {α : Type u} [linear_order α] (x y : α) :
y) =
@[simp, norm_cast]
theorem with_top.coe_max {α : Type u} [linear_order α] (x y : α) :
y) =
theorem with_top.well_founded_lt {α : Type u} [preorder α]  :
theorem with_top.well_founded_gt {α : Type u} [preorder α] (h : well_founded gt) :
theorem with_bot.well_founded_gt {α : Type u} [preorder α] (h : well_founded gt) :
@[protected, instance]
def with_top.trichotomous.lt {α : Type u} [preorder α]  :
@[protected, instance]
def with_top.is_well_order.lt {α : Type u} [preorder α] [h : has_lt.lt] :
@[protected, instance]
def with_top.trichotomous.gt {α : Type u} [preorder α]  :
@[protected, instance]
def with_top.is_well_order.gt {α : Type u} [preorder α] [h : gt] :
@[protected, instance]
def with_bot.trichotomous.lt {α : Type u} [preorder α] [h : has_lt.lt] :
@[protected, instance]
def with_bot.is_well_order.lt {α : Type u} [preorder α] [h : has_lt.lt] :
@[protected, instance]
def with_bot.trichotomous.gt {α : Type u} [preorder α] [h : gt] :
@[protected, instance]
def with_bot.is_well_order.gt {α : Type u} [preorder α] [h : gt] :
@[protected, instance]
def with_top.densely_ordered {α : Type u} [has_lt α] [no_max_order α] :
theorem with_top.lt_iff_exists_coe_btwn {α : Type u} [preorder α] [no_max_order α] {a b : with_top α} :
a < b ∃ (x : α), a < x x < b
@[protected, instance]
def with_top.no_bot_order {α : Type u} [has_le α] [no_bot_order α] [nonempty α] :
@[protected, instance]
def with_top.no_min_order {α : Type u} [has_lt α] [no_min_order α] [nonempty α] :
@[protected]
theorem monotone.with_bot_map {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : monotone f) :
@[protected]
theorem monotone.with_top_map {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : monotone f) :
@[protected]
theorem strict_mono.with_bot_map {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : strict_mono f) :
@[protected]
theorem strict_mono.with_top_map {α : Type u} {β : Type v} [preorder α] [preorder β] {f : α → β} (hf : strict_mono f) :

### 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 α] (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} [order_bot α] [order_bot (subtype p)] (hbot : p ) :
, hbot⟩ =
@[simp]
theorem subtype.mk_top {α : Type u} {p : α → Prop} [order_top α] [order_top (subtype p)] (htop : p ) :
, htop⟩ =
theorem subtype.coe_bot {α : Type u} {p : α → Prop} [order_bot α] [order_bot (subtype p)] (hbot : p ) :
theorem subtype.coe_top {α : Type u} {p : α → Prop} [order_top α] [order_top (subtype p)] (htop : p ) :
@[simp]
theorem subtype.coe_eq_bot_iff {α : Type u} {p : α → Prop} [order_bot α] [order_bot (subtype p)] (hbot : p ) {x : {x // p x}} :
@[simp]
theorem subtype.coe_eq_top_iff {α : Type u} {p : α → Prop} [order_top α] [order_top (subtype p)] (htop : p ) {x : {x // p x}} :
@[simp]
theorem subtype.mk_eq_bot_iff {α : Type u} {p : α → Prop} [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} [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 β]  :
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 : α} :
a = b =
@[simp]
theorem max_eq_top {α : Type u} [linear_order α] [order_top α] {a b : α} :
a = b =
@[simp]
theorem max_eq_bot {α : Type u} [linear_order α] [order_bot α] {a b : α} :
a = b =
@[simp]
theorem min_eq_top {α : Type u} [linear_order α] [order_top α] {a b : α} :
a = b =

### Disjointness and complements #

def disjoint {α : Type u} [order_bot α] (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
Instances for `disjoint`
theorem disjoint_iff {α : Type u} [order_bot α] {a b : α} :
b a b =
theorem disjoint.eq_bot {α : Type u} [order_bot α] {a b : α} :
ba b =
theorem disjoint.comm {α : Type u} [order_bot α] {a b : α} :
b a
@[symm]
theorem disjoint.symm {α : Type u} [order_bot α] ⦃a b : α⦄ :
b a
theorem symmetric_disjoint {α : Type u} [order_bot α] :
theorem disjoint_assoc {α : Type u} [order_bot α] {a b c : α} :
disjoint (a b) c (b c)
theorem disjoint_left_comm {α : Type u} [order_bot α] {a b c : α} :
(b c) (a c)
theorem disjoint_right_comm {α : Type u} [order_bot α] {a b c : α} :
disjoint (a b) c disjoint (a c) b
@[simp]
theorem disjoint_bot_left {α : Type u} [order_bot α] {a : α} :
@[simp]
theorem disjoint_bot_right {α : Type u} [order_bot α] {a : α} :
theorem disjoint.mono {α : Type u} [order_bot α] {a b c d : α} (h₁ : a b) (h₂ : c d) :
d c
theorem disjoint.mono_left {α : Type u} [order_bot α] {a b c : α} (h : a b) :
c c
theorem disjoint.mono_right {α : Type u} [order_bot α] {a b c : α} :
b c c b
theorem disjoint.inf_left {α : Type u} [order_bot α] {a b : α} (c : α) (h : b) :
disjoint (a c) b
theorem disjoint.inf_left' {α : Type u} [order_bot α] {a b : α} (c : α) (h : b) :
disjoint (c a) b
theorem disjoint.inf_right {α : Type u} [order_bot α] {a b : α} (c : α) (h : b) :
(b c)
theorem disjoint.inf_right' {α : Type u} [order_bot α] {a b : α} (c : α) (h : b) :
(c b)
@[simp]
theorem disjoint_self {α : Type u} [order_bot α] {a : α} :
a a =
theorem disjoint.eq_bot_of_self {α : Type u} [order_bot α] {a : α} :
aa =

Alias of the forward direction of `disjoint_self`.

theorem disjoint.ne {α : Type u} [order_bot α] {a b : α} (ha : a ) (hab : b) :
a b
theorem disjoint.eq_bot_of_le {α : Type u} [order_bot α] {a b : α} (hab : b) (h : a b) :
a =
theorem disjoint.eq_bot_of_ge {α : Type u} [order_bot α] {a b : α} (hab : b) :
b ab =
theorem disjoint.of_disjoint_inf_of_le {α : Type u} [order_bot α] {a b c : α} (h : disjoint (a b) c) (hle : a c) :
b
theorem disjoint.of_disjoint_inf_of_le' {α : Type u} [order_bot α] {a b c : α} (h : disjoint (a b) c) (hle : b c) :
b
@[simp]
theorem disjoint_top {α : Type u} [lattice α] {a : α} :
a =
@[simp]
theorem top_disjoint {α : Type u} [lattice α] {a : α} :
a =
@[simp]
theorem disjoint_sup_left {α : Type u} [order_bot α] {a b c : α} :
disjoint (a b) c c c
@[simp]
theorem disjoint_sup_right {α : Type u} [order_bot α] {a b c : α} :
(b c) b c
theorem disjoint.sup_left {α : Type u} [order_bot α] {a b c : α} (ha : c) (hb : c) :
disjoint (a b) c
theorem disjoint.sup_right {α : Type u} [order_bot α] {a b c : α} (hb : b) (hc : c) :
(b c)
theorem disjoint.left_le_of_le_sup_right {α : Type u} [order_bot α] {a b c : α} (h : a b c) (hd : c) :
a b
theorem disjoint.left_le_of_le_sup_left {α : Type u} [order_bot α] {a b c : α} (h : a c b) (hd : c) :
a b
def codisjoint {α : Type u} [order_top α] (a b : α) :
Prop

Two elements of a lattice are codisjoint if their sup is the top element.

Equations
theorem codisjoint_iff {α : Type u} [order_top α] {a b : α} :
b a b =
theorem codisjoint.eq_top {α : Type u} [order_top α] {a b : α} :
ba b =
theorem codisjoint.comm {α : Type u} [order_top α] {a b : α} :
b a
@[symm]
theorem codisjoint.symm {α : Type u} [order_top α] ⦃a b : α⦄ :
b a
theorem symmetric_codisjoint {α : Type u} [order_top α] :
theorem codisjoint_assoc {α : Type u} [order_top α] {a b c : α} :
codisjoint (a b) c (b c)
theorem codisjoint_left_comm {α : Type u} [order_top α] {a b c : α} :
(b c) (a c)
theorem codisjoint_right_comm {α : Type u} [order_top α] {a b c : α} :
codisjoint (a b) c codisjoint (a c) b
@[simp]
theorem codisjoint_top_left {α : Type u} [order_top α] {a : α} :
@[simp]
theorem codisjoint_top_right {α : Type u} [order_top α] {a : α} :
theorem codisjoint.mono {α : Type u} [order_top α] {a b c d : α} (h₁ : a b) (h₂ : c d) :
c d
theorem codisjoint.mono_left {α : Type u} [order_top α] {a b c : α} (h : a b) :
c c
theorem codisjoint.mono_right {α : Type u} [order_top α] {a b c : α} :
b c b c
theorem codisjoint.sup_left {α : Type u} [order_top α] {a b : α} (c : α) (h : b) :
codisjoint (a c) b
theorem codisjoint.sup_left' {α : Type u} [order_top α] {a b : α} (c : α) (h : b) :
codisjoint (c a) b
theorem codisjoint.sup_right {α : Type u} [order_top α] {a b : α} (c : α) (h : b) :
(b c)
theorem codisjoint.sup_right' {α : Type u} [order_top α] {a b : α} (c : α) (h : b) :
(c b)
@[simp]
theorem codisjoint_self {α : Type u} [order_top α] {a : α} :
a a =
theorem codisjoint.eq_top_of_self {α : Type u} [order_top α] {a : α} :
aa =

Alias of the forward direction of `codisjoint_self`.

theorem codisjoint.ne {α : Type u} [order_top α] {a b : α} (ha : a ) (hab : b) :
a b
theorem codisjoint.eq_top_of_ge {α : Type u} [order_top α] {a b : α} (hab : b) (h : b a) :
a =
theorem codisjoint.eq_top_of_le {α : Type u} [order_top α] {a b : α} (hab : b) :
a bb =
theorem codisjoint.of_codisjoint_sup_of_le {α : Type u} [order_top α] {a b c : α} (h : codisjoint (a b) c) (hle : c a) :
b
theorem codisjoint.of_codisjoint_sup_of_le' {α : Type u} [order_top α] {a b c : α} (h : codisjoint (a b) c) (hle : c b) :
b
@[simp]
theorem codisjoint_bot {α : Type u} [lattice α] {a : α} :
a =
@[simp]
theorem bot_codisjoint {α : Type u} [lattice α] {a : α} :
a =
@[simp]
theorem codisjoint_inf_left {α : Type u} [order_top α] {a b c : α} :
codisjoint (a b) c c c
@[simp]
theorem codisjoint_inf_right {α : Type u} [order_top α] {a b c : α} :
(b c) b c
theorem codisjoint.inf_left {α : Type u} [order_top α] {a b c : α} (ha : c) (hb : c) :
codisjoint (a b) c
theorem codisjoint.inf_right {α : Type u} [order_top α] {a b c : α} (hb : b) (hc : c) :
(b c)
theorem codisjoint.left_le_of_le_inf_right {α : Type u} [order_top α] {a b c : α} (h : a b c) (hd : c) :
a c
theorem codisjoint.left_le_of_le_inf_left {α : Type u} [order_top α] {a b c : α} (h : b a c) (hd : c) :
a c
theorem disjoint.dual {α : Type u} [order_bot α] {a b : α} :
b
theorem codisjoint.dual {α : Type u} [order_top α] {a b : α} :
b
@[simp]
theorem disjoint_to_dual_iff {α : Type u} [order_top α] {a b : α} :
@[simp]
theorem disjoint_of_dual_iff {α : Type u} [order_bot α] {a b : αᵒᵈ} :
@[simp]
theorem codisjoint_to_dual_iff {α : Type u} [order_bot α] {a b : α} :
@[simp]
theorem codisjoint_of_dual_iff {α : Type u} [order_top α] {a b : αᵒᵈ} :
theorem disjoint.le_of_codisjoint {α : Type u} {a b c : α} (hab : b) (hbc : c) :
a c
structure is_compl {α : Type u} [lattice α] (x y : α) :
Prop
• disjoint : y
• codisjoint : y

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

@[protected, symm]
theorem is_compl.symm {α : Type u} [lattice α] {x y : α} (h : y) :
x
theorem is_compl.of_eq {α : Type u} [lattice α] {x y : α} (h₁ : x y = ) (h₂ : x y = ) :
y
theorem is_compl.inf_eq_bot {α : Type u} [lattice α] {x y : α} (h : y) :
x y =
theorem is_compl.sup_eq_top {α : Type u} [lattice α] {x y : α} (h : y) :
x y =
theorem is_compl.dual {α : Type u} [lattice α] {x y : α} (h : y) :
theorem is_compl.of_dual {α : Type u} [lattice α] {a b : αᵒᵈ} (h : b) :
theorem is_compl.inf_left_le_of_le_sup_right {α : Type u} {a b x y : α} (h : y) (hle : a b y) :
a x b
theorem is_compl.le_sup_right_iff_inf_left_le {α : Type u} {x y a b : α} (h : y) :
a b y a x b
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
@[protected]
theorem is_compl.antitone {α : 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')
@[simp]
theorem is_compl_to_dual_iff {α : Type u} [lattice α] {a b : α} :
b
@[simp]
theorem is_compl_of_dual_iff {α : Type u} [lattice α] {a b : αᵒᵈ} :
b
theorem is_compl_bot_top {α : Type u} [lattice α]  :
theorem is_compl_top_bot {α : Type u} [lattice α]  :
theorem eq_top_of_is_compl_bot {α : Type u} [lattice α] {x : α} (h : ) :
x =
theorem eq_top_of_bot_is_compl {α : Type u} [lattice α] {x : α} (h : x) :
x =
theorem eq_bot_of_is_compl_top {α : Type u} [lattice α] {x : α} (h : ) :
x =
theorem eq_bot_of_top_is_compl {α : Type u} [lattice α] {x : α} (h : x) :
x =
@[class]
structure complemented_lattice (α : Type u_1) [lattice α]  :
Prop
• exists_is_compl : ∀ (a : α), ∃ (b : α), b

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

Instances of this typeclass
@[protected, instance]