mathlib documentation

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 #

Common lattices #

Implementation notes #

We didn't prove things about [distrib_lattice α] [order_top α] because the dual notion of disjoint isn't really used anywhere.

Top, bottom element #

@[protected, instance]
def has_top_nonempty (α : Type u) [has_top α] :
@[protected, instance]
def has_bot_nonempty (α : Type u) [has_bot α] :
@[instance]
def order_top.to_has_top (α : Type u) [has_le α] [self : order_top α] :
@[simp]
theorem le_top {α : Type u} [has_le α] [order_top α] {a : α} :
@[simp]
theorem is_top_top {α : Type u} [has_le α] [order_top α] :
@[simp]
theorem is_max_top {α : Type u} [preorder α] [order_top α] :
@[simp]
theorem not_top_lt {α : Type u} [preorder α] [order_top α] {a : α} :
theorem ne_top_of_lt {α : Type u} [preorder α] [order_top α] {a b : α} (h : a < b) :
theorem has_lt.lt.ne_top {α : Type u} [preorder α] [order_top α] {a b : α} (h : a < b) :

Alias of ne_top_of_lt.

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

Alias of is_max_iff_eq_top.

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

Alias of is_top_iff_eq_top.

@[simp]
theorem top_le_iff {α : Type u} [partial_order α] [order_top α] {a : α} :
theorem top_unique {α : Type u} [partial_order α] [order_top α] {a : α} (h : a) :
a =
theorem eq_top_iff {α : Type u} [partial_order α] [order_top α] {a : α} :
theorem eq_top_mono {α : Type u} [partial_order α] [order_top α] {a b : α} (h : a b) (h₂ : a = ) :
b =
theorem lt_top_iff_ne_top {α : Type u} [partial_order α] [order_top α] {a : α} :
@[simp]
theorem not_lt_top_iff {α : Type u} [partial_order α] [order_top α] {a : α} :
theorem eq_top_or_lt_top {α : Type u} [partial_order α] [order_top α] (a : α) :
a = a <
theorem ne.lt_top {α : Type u} [partial_order α] [order_top α] {a : α} (h : a ) :
a <
theorem ne.lt_top' {α : Type u} [partial_order α] [order_top α] {a : α} (h : a) :
a <
theorem ne_top_of_le_ne_top {α : Type u} [partial_order α] [order_top α] {a b : α} (hb : b ) (hab : a b) :
theorem strict_mono.apply_eq_top_iff {α : Type u} {β : Type v} [partial_order α] [order_top α] [preorder β] {f : α → β} {a : α} (hf : strict_mono f) :
f a = f a =
theorem strict_anti.apply_eq_top_iff {α : Type u} {β : Type v} [partial_order α] [order_top α] [preorder β] {f : α → β} {a : α} (hf : strict_anti f) :
f a = f a =
theorem not_is_min_top {α : Type u} [partial_order α] [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} [partial_order α] {A B : order_top α} :
A = B
@[instance]
def order_bot.to_has_bot (α : Type u) [has_le α] [self : order_bot α] :
@[simp]
theorem bot_le {α : Type u} [has_le α] [order_bot α] {a : α} :
@[simp]
theorem is_bot_bot {α : Type u} [has_le α] [order_bot α] :
@[simp]
theorem is_min_bot {α : Type u} [preorder α] [order_bot α] :
@[simp]
theorem not_lt_bot {α : Type u} [preorder α] [order_bot α] {a : α} :
theorem ne_bot_of_gt {α : Type u} [preorder α] [order_bot α] {a b : α} (h : a < b) :
theorem has_lt.lt.ne_bot {α : Type u} [preorder α] [order_bot α] {a b : α} (h : a < b) :

Alias of ne_bot_of_gt.

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

Alias of is_min_iff_eq_bot.

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

Alias of is_bot_iff_eq_bot.

@[simp]
theorem le_bot_iff {α : Type u} [partial_order α] [order_bot α] {a : α} :
theorem bot_unique {α : Type u} [partial_order α] [order_bot α] {a : α} (h : a ) :
a =
theorem eq_bot_iff {α : Type u} [partial_order α] [order_bot α] {a : α} :
theorem eq_bot_mono {α : Type u} [partial_order α] [order_bot α] {a b : α} (h : a b) (h₂ : b = ) :
a =
theorem bot_lt_iff_ne_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :
@[simp]
theorem not_bot_lt_iff {α : Type u} [partial_order α] [order_bot α] {a : α} :
theorem eq_bot_or_bot_lt {α : Type u} [partial_order α] [order_bot α] (a : α) :
a = < a
theorem eq_bot_of_minimal {α : Type u} [partial_order α] [order_bot α] {a : α} (h : ∀ (b : α), ¬b < a) :
a =
theorem ne.bot_lt {α : Type u} [partial_order α] [order_bot α] {a : α} (h : a ) :
< a
theorem ne.bot_lt' {α : Type u} [partial_order α] [order_bot α] {a : α} (h : a) :
< a
theorem ne_bot_of_le_ne_bot {α : Type u} [partial_order α] [order_bot α] {a b : α} (hb : b ) (hab : b a) :
theorem strict_mono.apply_eq_bot_iff {α : Type u} {β : Type v} [partial_order α] [order_bot α] [preorder β] {f : α → β} {a : α} (hf : strict_mono f) :
f a = f a =
theorem strict_anti.apply_eq_bot_iff {α : Type u} {β : Type v} [partial_order α] [order_bot α] [preorder β] {f : α → β} {a : α} (hf : strict_anti f) :
f a = f a =
theorem not_is_max_bot {α : Type u} [partial_order α] [order_bot α] [nontrivial α] :
theorem strict_mono.minimal_preimage_bot {α : Type u} {β : Type v} [linear_order α] [partial_order β] [order_bot β] {f : α → β} (H : strict_mono f) {a : α} (h_bot : f a = ) (x : α) :
a x
theorem order_bot.ext_bot {α : Type u_1} {hA : partial_order α} (A : order_bot α) {hB : partial_order α} (B : order_bot α) (H : ∀ (x y : α), x y x y) :
theorem order_bot.ext {α : Type u_1} [partial_order α] {A B : order_bot α} :
A = B
@[simp]
theorem top_sup_eq {α : Type u} [semilattice_sup α] [order_top α] {a : α} :
@[simp]
theorem sup_top_eq {α : Type u} [semilattice_sup α] [order_top α] {a : α} :
@[simp]
theorem bot_sup_eq {α : Type u} [semilattice_sup α] [order_bot α] {a : α} :
a = a
@[simp]
theorem sup_bot_eq {α : Type u} [semilattice_sup α] [order_bot α] {a : α} :
a = a
@[simp]
theorem sup_eq_bot_iff {α : Type u} [semilattice_sup α] [order_bot α] {a b : α} :
a b = a = b =
@[simp]
theorem top_inf_eq {α : Type u} [semilattice_inf α] [order_top α] {a : α} :
a = a
@[simp]
theorem inf_top_eq {α : Type u} [semilattice_inf α] [order_top α] {a : α} :
a = a
@[simp]
theorem inf_eq_top_iff {α : Type u} [semilattice_inf α] [order_top α] {a b : α} :
a b = a = b =
@[simp]
theorem bot_inf_eq {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :
@[simp]
theorem inf_bot_eq {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :

Bounded order #

@[instance]
def bounded_order.to_order_bot (α : Type u) [has_le α] [self : bounded_order α] :
@[instance]
def bounded_order.to_order_top (α : Type u) [has_le α] [self : bounded_order α] :
theorem bounded_order.ext {α : Type u_1} [partial_order α] {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 le_Prop_eq  :
has_le.le = λ (_x _y : Prop), _x → _y
@[simp]
theorem sup_Prop_eq  :
@[simp]

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} [semilattice_sup α] {P : α → Prop} {x₀ : α} (hP : monotone P) :
(∃ (x : α), x₀ x P x) ∃ (x : α), P x
theorem exists_le_and_iff_exists {α : Type u} [semilattice_inf α] {P : α → Prop} {x₀ : α} (hP : antitone P) :
(∃ (x : α), x x₀ P x) ∃ (x : α), P x

Function lattices #

@[protected, instance]
def pi.has_bot {ι : Type u_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} [partial_order α] [bounded_order α] (hα : = ) (x : α) :
x =
theorem eq_top_of_bot_eq_top {α : Type u} [partial_order α] [bounded_order α] (hα : = ) (x : α) :
x =
theorem subsingleton_of_top_le_bot {α : Type u} [partial_order α] [bounded_order α] (h : ) :
theorem subsingleton_of_bot_eq_top {α : Type u} [partial_order α] [bounded_order α] (hα : = ) :
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
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
def bounded_order.lift {α : Type u} {β : Type v} [has_le α] [has_top α] [has_bot α] [has_le β] [bounded_order β] (f : α → β) (map_le : ∀ (a b : α), f a f 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
@[protected, instance]
meta def with_bot.has_to_format {α : Type u} [has_to_format α] :
@[protected, instance]
def with_bot.has_repr {α : Type u} [has_repr α] :
Equations
@[protected, instance]
def with_bot.has_coe_t {α : Type u} :
Equations
@[protected, instance]
def with_bot.has_bot {α : Type u} :
Equations
@[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 : 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
@[norm_cast]
theorem with_bot.coe_eq_coe {α : Type u} {a b : α} :
a = b a = b
@[simp]
theorem with_bot.map_bot {α : Type u} {β : Type v} (f : α → β) :
theorem with_bot.map_coe {α : Type u} {β : Type v} (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 α] :
some a some b 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
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 α] :
some a < some b 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
theorem with_bot.le_coe_get_or_else {α : Type u} [preorder α] (a : with_bot α) (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 : α} :
theorem with_bot.coe_sup {α : Type u} [semilattice_sup α] (a b : α) :
(a b) = a b
@[protected, instance]
Equations
theorem with_bot.coe_inf {α : Type u} [semilattice_inf α] (a b : α) :
(a b) = a b
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[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 : α) :
(min x y) = min x y
@[norm_cast]
theorem with_bot.coe_max {α : Type u} [linear_order α] (x y : α) :
(max x y) = max x y
@[protected, instance]
theorem with_bot.lt_iff_exists_coe_btwn {α : Type u} [preorder α] [densely_ordered α] [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
@[protected, instance]
meta def with_top.has_to_format {α : Type u} [has_to_format α] :
@[protected, instance]
def with_top.has_repr {α : Type u} [has_repr α] :
Equations
@[protected, instance]
def with_top.has_coe_t {α : Type u} :
Equations
@[protected, instance]
def with_top.has_top {α : Type u} :
Equations
@[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 : 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
@[norm_cast]
theorem with_top.coe_eq_coe {α : Type u} {a b : α} :
a = b a = b
@[simp]
theorem with_top.map_top {α : Type u} {β : Type v} (f : α → β) :
theorem with_top.map_coe {α : Type u} {β : Type v} (f : α → β) (a : α) :
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
@[simp]
theorem with_top.some_le_some {α : Type u} {a b : α} [has_le α] :
some a some b a b
@[simp, norm_cast]
theorem with_top.coe_le_coe {α : Type u} {a b : α} [has_le α] :
a b 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
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
@[simp]
theorem with_top.some_lt_some {α : Type u} {a b : α} [has_lt α] :
some a < some b a < b
@[simp, norm_cast]
theorem with_top.coe_lt_coe {α : Type u} {a b : α} [has_lt α] :
a < b a < b
@[simp]
theorem with_top.some_lt_none {α : Type u} [has_lt α] (a : α) :
theorem with_top.coe_lt_top {α : 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} {a : α} [has_lt α] {x : with_top α} :
a < x ∀ (b : α), x = ba < b
@[protected, instance]
def with_top.preorder {α : Type u} [preorder α] :
Equations
theorem with_top.coe_inf {α : Type u} [semilattice_inf α] (a b : α) :
(a b) = a b
@[protected, instance]
Equations
theorem with_top.coe_sup {α : Type u} [semilattice_sup α] (a b : α) :
(a b) = a b
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[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 : α) :
(min x y) = min x y
@[simp, norm_cast]
theorem with_top.coe_max {α : Type u} [linear_order α] (x y : α) :
(max x y) = max x y
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]
theorem with_top.lt_iff_exists_coe_btwn {α : Type u} [preorder α] [densely_ordered α] [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 α] :

Subtype, order dual, product lattices #

@[protected]
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]
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]
def subtype.bounded_order {α : Type u} {p : α → Prop} [has_le α] [bounded_order α] (hbot : p ) (htop : p ) :

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

Equations
@[simp]
theorem subtype.mk_bot {α : Type u} {p : α → Prop} [partial_order α] [order_bot α] [order_bot (subtype p)] (hbot : p ) :
, hbot⟩ =
@[simp]
theorem subtype.mk_top {α : Type u} {p : α → Prop} [partial_order α] [order_top α] [order_top (subtype p)] (htop : p ) :
, htop⟩ =
theorem subtype.coe_bot {α : Type u} {p : α → Prop} [partial_order α] [order_bot α] [order_bot (subtype p)] (hbot : p ) :
theorem subtype.coe_top {α : Type u} {p : α → Prop} [partial_order α] [order_top α] [order_top (subtype p)] (htop : p ) :
@[simp]
theorem subtype.coe_eq_bot_iff {α : Type u} {p : α → Prop} [partial_order α] [order_bot α] [order_bot (subtype p)] (hbot : p ) {x : {x // p x}} :
@[simp]
theorem subtype.coe_eq_top_iff {α : Type u} {p : α → Prop} [partial_order α] [order_top α] [order_top (subtype p)] (htop : p ) {x : {x // p x}} :
@[simp]
theorem subtype.mk_eq_bot_iff {α : Type u} {p : α → Prop} [partial_order α] [order_bot α] [order_bot (subtype p)] (hbot : p ) {x : α} (hx : p x) :
x, hx⟩ = x =
@[simp]
theorem subtype.mk_eq_top_iff {α : Type u} {p : α → Prop} [partial_order α] [order_top α] [order_top (subtype p)] (htop : p ) {x : α} (hx : p x) :
x, hx⟩ = x =
@[protected, instance]
def 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
@[protected, instance]
def prod.has_top (α : Type u) (β : Type v) [has_top α] [has_top β] :
has_top × β)
Equations
@[protected, instance]
def prod.has_bot (α : Type u) (β : Type v) [has_bot α] [has_bot β] :
has_bot × β)
Equations
@[protected, instance]
def prod.order_top (α : Type u) (β : Type v) [has_le α] [has_le β] [order_top α] [order_top β] :
order_top × β)
Equations
@[protected, instance]
def prod.order_bot (α : Type u) (β : Type v) [has_le α] [has_le β] [order_bot α] [order_bot β] :
order_bot × β)
Equations
@[protected, instance]
def prod.bounded_order (α : Type u) (β : Type v) [has_le α] [has_le β] [bounded_order α] [bounded_order β] :
Equations

Disjointness and complements #

def disjoint {α : Type u} [semilattice_inf α] [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
theorem disjoint.eq_bot {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (h : disjoint a b) :
a b =
theorem disjoint_iff {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} :
disjoint a b a b =
theorem disjoint.comm {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} :
theorem disjoint.symm {α : Type u} [semilattice_inf α] [order_bot α] ⦃a b : α⦄ :
disjoint a bdisjoint b a
@[simp]
theorem disjoint_bot_left {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :
@[simp]
theorem disjoint_bot_right {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :
theorem disjoint.mono {α : Type u} [semilattice_inf α] [order_bot α] {a b c d : α} (h₁ : a b) (h₂ : c d) :
disjoint b ddisjoint a c
theorem disjoint.mono_left {α : Type u} [semilattice_inf α] [order_bot α] {a b c : α} (h : a b) :
disjoint b cdisjoint a c
theorem disjoint.mono_right {α : Type u} [semilattice_inf α] [order_bot α] {a b c : α} (h : b c) :
disjoint a cdisjoint a b
@[simp]
theorem disjoint_self {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :
theorem disjoint.ne {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (ha : a ) (hab : disjoint a b) :
a b
theorem disjoint.eq_bot_of_le {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (hab : disjoint a b) (h : a b) :
a =
theorem disjoint_assoc {α : Type u} [semilattice_inf α] [order_bot α] {a b c : α} :
disjoint (a b) c disjoint a (b c)
theorem disjoint.of_disjoint_inf_of_le {α : Type u} [semilattice_inf α] [order_bot α] {a b c : α} (h : disjoint (a b) c) (hle : a c) :
theorem disjoint.of_disjoint_inf_of_le' {α : Type u} [semilattice_inf α] [order_bot α] {a b c : α} (h : disjoint (a b) c) (hle : b c) :
theorem eq_bot_of_disjoint_absorbs {α : Type u} [lattice α] [order_bot α] {a b : α} (w : disjoint a b) (h : a b = a) :
b =
@[simp]
theorem disjoint_top {α : Type u} [lattice α] [bounded_order α] {a : α} :
@[simp]
theorem top_disjoint {α : Type u} [lattice α] [bounded_order α] {a : α} :
theorem min_top_left {α : Type u} [linear_order α] [order_top α] (a : α) :
min a = a
theorem min_top_right {α : Type u} [linear_order α] [order_top α] (a : α) :
min a = a
theorem max_bot_left {α : Type u} [linear_order α] [order_bot α] (a : α) :
max a = a
theorem max_bot_right {α : Type u} [linear_order α] [order_bot α] (a : α) :
max a = a
theorem min_bot_left {α : Type u} [linear_order α] [order_bot α] (a : α) :
theorem min_bot_right {α : Type u} [linear_order α] [order_bot α] (a : α) :
theorem max_top_left {α : Type u} [linear_order α] [order_top α] (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 : α} :
min a b = a = b =
@[simp]
theorem max_eq_top {α : Type u} [linear_order α] [order_top α] {a b : α} :
max a b = a = b =
@[simp]
theorem max_eq_bot {α : Type u} [linear_order α] [order_bot α] {a b : α} :
max a b = a = b =
@[simp]
theorem min_eq_top {α : Type u} [linear_order α] [order_top α] {a b : α} :
min a b = a = b =
@[simp]
theorem disjoint_sup_left {α : Type u} [distrib_lattice α] [order_bot α] {a b c : α} :
@[simp]
theorem disjoint_sup_right {α : Type u} [distrib_lattice α] [order_bot α] {a b c : α} :
theorem disjoint.sup_left {α : Type u} [distrib_lattice α] [order_bot α] {a b c : α} (ha : disjoint a c) (hb : disjoint b c) :
disjoint (a b) c
theorem disjoint.sup_right {α : Type u} [distrib_lattice α] [order_bot α] {a b c : α} (hb : disjoint a b) (hc : disjoint a c) :
disjoint a (b c)
theorem disjoint.left_le_of_le_sup_right {α : Type u} [distrib_lattice α] [order_bot α] {a b c : α} (h : a b c) (hd : disjoint a c) :
a b
theorem disjoint.left_le_of_le_sup_left {α : Type u} [distrib_lattice α] [order_bot α] {a b c : α} (h : a c b) (hd : disjoint a c) :
a b
theorem disjoint.inf_left {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (c : α) (h : disjoint a b) :
disjoint (a c) b
theorem disjoint.inf_left' {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (c : α) (h : disjoint a b) :
disjoint (c a) b
theorem disjoint.inf_right {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (c : α) (h : disjoint a b) :
disjoint a (b c)
theorem disjoint.inf_right' {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (c : α) (h : disjoint a b) :
disjoint a (c b)
theorem inf_eq_bot_iff_le_compl {α : Type u} [distrib_lattice α] [bounded_order α] {a b c : α} (h₁ : b c = ) (h₂ : b c = ) :
a b = a c
structure is_compl {α : Type u} [lattice α] [bounded_order α] (x y : α) :
Prop

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

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

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

Instances
@[protected, instance]
theorem bot_ne_top {α : Type u} [partial_order α] [bounded_order α] [nontrivial α] :
theorem top_ne_bot {α : Type u} [partial_order α] [bounded_order α] [nontrivial α] :
theorem bot_lt_top {α : Type u} [partial_order α] [bounded_order α] [nontrivial α] :
@[protected, instance]
Equations
@[simp]
theorem top_eq_tt  :
@[simp]
theorem bot_eq_ff  :