mathlib documentation

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 #

Implementation notes #

We didn't define distrib_lattice_top because the dual notion of disjoint isn't really used anywhere.

Top, bottom element #

@[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 : α), a bb ca c
  • 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 : α} :
@[simp]
theorem is_top_iff_eq_top {α : 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 has_lt.lt.ne_top {α : Type u} [order_top α] {a b : α} (h : a < b) :

Alias of ne_top_of_lt.

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 ne.lt_top {α : Type u} [order_top α] {a : α} (h : a ) :
a <
theorem ne.lt_top' {α : Type u} [order_top α] {a : α} (h : a) :
a <
theorem strict_mono.maximal_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
@[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 : α} :
@[simp]
theorem is_bot_iff_eq_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 has_lt.lt.ne_bot {α : Type u} [order_bot α] {a b : α} (h : a < b) :

Alias of ne_bot_of_gt.

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 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} {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 : α), a bb ca c
  • 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 : α), a cb ca b c

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} [semilattice_sup_top α] {a : α} :
@[simp]
theorem sup_top_eq {α : Type u} [semilattice_sup_top α] {a : α} :
@[instance]
def semilattice_sup_bot.to_order_bot (α : Type u) [self : semilattice_sup_bot α] :
@[instance]
@[simp]
theorem bot_sup_eq {α : Type u} [semilattice_sup_bot α] {a : α} :
a = a
@[simp]
theorem sup_bot_eq {α : Type u} [semilattice_sup_bot α] {a : α} :
a = a
@[simp]
theorem sup_eq_bot_iff {α : Type u} [semilattice_sup_bot α] {a b : α} :
a b = a = b =
@[class]
structure semilattice_inf_top (α : Type u) :
Type u
  • top : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • 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 : α), a ba ca b c

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} [semilattice_inf_top α] {a : α} :
a = a
@[simp]
theorem inf_top_eq {α : Type u} [semilattice_inf_top α] {a : α} :
a = a
@[simp]
theorem inf_eq_top_iff {α : Type u} [semilattice_inf_top α] {a b : α} :
a b = a = b =
@[instance]
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 : α), a bb ca c
  • 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 : α), a ba ca b c

A semilattice_inf_bot is a semilattice with bottom and meet.

Instances
@[instance]
@[simp]
theorem bot_inf_eq {α : Type u} [semilattice_inf_bot α] {a : α} :
@[simp]
theorem inf_bot_eq {α : Type u} [semilattice_inf_bot α] {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 : α), a bb ca c
  • 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 : α), a cb ca b c
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c : α), a ba ca b c
  • top : α
  • le_top : ∀ (a : α), a
  • bot : α
  • bot_le : ∀ (a : α), a

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

Instances
theorem bounded_lattice.ext {α : Type u_1} {A B : bounded_lattice α} (H : ∀ (x y : α), x y x y) :
A = B
@[instance]
@[class]
structure distrib_lattice_bot (α : Type u_1) :
Type u_1
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • 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 : α), a cb ca b c
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c : α), a ba ca b c
  • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z
  • bot : α
  • bot_le : ∀ (a : α), a

A distrib_lattice_bot is a distributive lattice with a least element.

Instances
@[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 : α), a bb ca c
  • 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 : α), a cb ca b c
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c : α), a ba ca b c
  • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z
  • bot : α
  • bot_le : ∀ (a : α), a
  • top : α
  • le_top : ∀ (a : α), a

A bounded distributive lattice is exactly what it sounds like.

Instances
theorem inf_eq_bot_iff_le_compl {α : Type u} [bounded_distrib_lattice α] {a b c : α} (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 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_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 : ι),
@[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 : ι),
@[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
theorem eq_bot_of_bot_eq_top {α : Type u_1} [bounded_lattice α] (hα : = ) (x : α) :
x =
theorem eq_top_of_bot_eq_top {α : Type u_1} [bounded_lattice α] (hα : = ) (x : α) :
x =
theorem subsingleton_of_top_le_bot {α : Type u_1} [bounded_lattice α] (h : ) :
theorem subsingleton_of_bot_eq_top {α : Type u_1} [bounded_lattice α] (hα : = ) :

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} [has_to_format α] :
@[instance]
def with_bot.has_coe_t {α : Type u} :
Equations
@[instance]
def with_bot.has_bot {α : Type u} :
Equations
@[instance]
def with_bot.inhabited {α : Type u} :
Equations
theorem with_bot.none_eq_bot {α : Type u} :
theorem with_bot.some_eq_coe {α : Type u} (a : α) :
@[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
theorem with_bot.coe_eq_coe {α : Type u} {a b : α} :
a = b a = b
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_1} (x : with_bot α) (h : x ) :
(x.unbot h) = x
@[simp]
theorem with_bot.unbot_coe {α : Type u} (x : α) (h : x := _) :
x.unbot h = x
@[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.none_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
@[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} [preorder α] {a b : α} {o : option α} :
b o(a o a b)
theorem with_bot.coe_lt_coe {α : Type u} [preorder α] {a b : α} :
a < b a < b
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} [order_bot α] {a : with_bot α} {b : α} :
@[instance]
Equations
theorem with_bot.coe_sup {α : Type u} [semilattice_sup α] (a b : α) :
(a b) = a b
@[instance]
Equations
theorem with_bot.coe_inf {α : Type u} [semilattice_inf α] (a b : α) :
(a b) = a b
@[instance]
def with_bot.linear_order {α : Type u} [linear_order α] :
Equations
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
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} [has_to_format α] :
@[instance]
def with_top.has_coe_t {α : Type u} :
Equations
@[instance]
def with_top.has_top {α : Type u} :
Equations
@[instance]
def with_top.inhabited {α : Type u} :
Equations
theorem with_top.none_eq_top {α : Type u} :
theorem with_top.some_eq_coe {α : Type u} (a : α) :
def with_top.rec_top_coe {α : Type u} {C : with_top αSort u_1} (h₁ : C ) (h₂ : Π (a : α), C a) (n : with_top α) :
C n

Recursor for with_top using the preferred forms and ↑a.

Equations
theorem with_top.coe_eq_coe {α : Type u} {a b : α} :
a = b a = b
@[simp]
theorem with_top.top_ne_coe {α : Type u} {a : α} :
@[simp]
theorem with_top.coe_ne_top {α : Type u} {a : α} :
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_1} (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
@[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
@[simp]
theorem with_top.coe_le_coe {α : Type u} [preorder α] {a b : α} :
a b a b
theorem with_top.le_coe {α : Type u} [preorder α] {a b : α} {o : option α} :
a o(o b a b)
theorem with_top.le_coe_iff {α : Type u} [partial_order α] {b : α} {x : with_top α} :
x b ∃ (a : α), x = a a b
theorem with_top.coe_le_iff {α : Type u} [partial_order α] {a : α} {x : with_top α} :
a x ∀ (b : α), x = ba b
theorem with_top.lt_iff_exists_coe {α : Type u} [partial_order α] {a b : with_top α} :
a < b ∃ (p : α), a = p p < b
theorem with_top.coe_lt_coe {α : Type u} [preorder α] {a b : α} :
a < b a < b
theorem with_top.coe_lt_top {α : Type u} [preorder α] (a : α) :
theorem with_top.coe_lt_iff {α : Type u} [preorder α] {a : α} {x : with_top α} :
a < x ∀ (b : α), x = ba < b
theorem with_top.not_top_le_coe {α : Type u} [preorder α] (a : α) :
theorem with_top.coe_inf {α : Type u} [semilattice_inf α] (a b : α) :
(a b) = a b
@[instance]
Equations
theorem with_top.coe_sup {α : Type u} [semilattice_sup α] (a b : α) :
(a b) = a b
@[instance]
def with_top.linear_order {α : Type u} [linear_order α] :
Equations
@[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
theorem with_top.lt_iff_exists_coe_btwn {α : Type u} [partial_order α] [densely_ordered α] [no_top_order α] {a b : with_top α} :
a < b ∃ (x : α), a < x x < b

Subtype, order dual, product lattices #

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

A subtype forms a --semilattice if and preserve the property. See note [reducible non-instances].

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

A subtype forms a --semilattice if and preserve the property. See note [reducible non-instances].

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

A subtype forms a --semilattice if and preserve the property. See note [reducible non-instances].

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

A subtype forms a --semilattice if and preserve the property. See note [reducible non-instances].

Equations
@[instance]
def order_dual.has_top (α : Type u) [has_bot α] :
Equations
@[instance]
def order_dual.has_bot (α : Type u) [has_top α] :
Equations
@[instance]
def prod.has_top (α : Type u) (β : Type v) [has_top α] [has_top β] :
has_top × β)
Equations
@[instance]
def prod.has_bot (α : Type u) (β : Type v) [has_bot α] [has_bot β] :
has_bot × β)
Equations
@[instance]
def prod.order_top (α : Type u) (β : Type v) [order_top α] [order_top β] :
order_top × β)
Equations
@[instance]
def prod.order_bot (α : Type u) (β : Type v) [order_bot α] [order_bot β] :
order_bot × β)
Equations
@[instance]
def prod.bounded_lattice (α : Type u) (β : Type v) [bounded_lattice α] [bounded_lattice β] :
Equations

Disjointness and complements #

def disjoint {α : Type u} [semilattice_inf_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_bot α] {a b : α} (h : disjoint a b) :
a b =
theorem disjoint_iff {α : Type u} [semilattice_inf_bot α] {a b : α} :
disjoint a b a b =
theorem disjoint.comm {α : Type u} [semilattice_inf_bot α] {a b : α} :
theorem disjoint.symm {α : Type u} [semilattice_inf_bot α] ⦃a b : α⦄ :
disjoint a bdisjoint b a
@[simp]
theorem disjoint_bot_left {α : Type u} [semilattice_inf_bot α] {a : α} :
@[simp]
theorem disjoint_bot_right {α : Type u} [semilattice_inf_bot α] {a : α} :
theorem disjoint.mono {α : Type u} [semilattice_inf_bot α] {a b c d : α} (h₁ : a b) (h₂ : c d) :
disjoint b ddisjoint a c
theorem disjoint.mono_left {α : Type u} [semilattice_inf_bot α] {a b c : α} (h : a b) :
disjoint b cdisjoint a c
theorem disjoint.mono_right {α : Type u} [semilattice_inf_bot α] {a b c : α} (h : b c) :
disjoint a cdisjoint a b
@[simp]
theorem disjoint_self {α : Type u} [semilattice_inf_bot α] {a : α} :
theorem disjoint.ne {α : Type u} [semilattice_inf_bot α] {a b : α} (ha : a ) (hab : disjoint a b) :
a b
theorem disjoint.eq_bot_of_le {α : Type u} [semilattice_inf_bot α] {a b : α} (hab : disjoint a b) (h : a b) :
a =
theorem disjoint.of_disjoint_inf_of_le {α : Type u} [semilattice_inf_bot α] {a b c : α} (h : disjoint (a b) c) (hle : a c) :
theorem disjoint.of_disjoint_inf_of_le' {α : Type u} [semilattice_inf_bot α] {a b c : α} (h : disjoint (a b) c) (hle : b c) :
@[simp]
theorem disjoint_top {α : Type u} [bounded_lattice α] {a : α} :
@[simp]
theorem top_disjoint {α : Type u} [bounded_lattice α] {a : α} :
theorem eq_bot_of_disjoint_absorbs {α : Type u} [bounded_lattice α] {a b : α} (w : disjoint a b) (h : a b = a) :
b =
@[simp]
theorem disjoint_sup_left {α : Type u} [distrib_lattice_bot α] {a b c : α} :
@[simp]
theorem disjoint_sup_right {α : Type u} [distrib_lattice_bot α] {a b c : α} :
theorem disjoint.sup_left {α : Type u} [distrib_lattice_bot α] {a b c : α} (ha : disjoint a c) (hb : disjoint b c) :
disjoint (a b) c
theorem disjoint.sup_right {α : Type u} [distrib_lattice_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_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_bot α] {a b c : α} (h : a c b) (hd : disjoint a c) :
a b
theorem disjoint.inf_left {α : Type u} [semilattice_inf_bot α] {a b : α} (c : α) (h : disjoint a b) :
disjoint (a c) b
theorem disjoint.inf_left' {α : Type u} [semilattice_inf_bot α] {a b : α} (c : α) (h : disjoint a b) :
disjoint (c a) b
theorem disjoint.inf_right {α : Type u} [semilattice_inf_bot α] {a b : α} (c : α) (h : disjoint a b) :
disjoint a (b c)
theorem disjoint.inf_right' {α : Type u} [semilattice_inf_bot α] {a b : α} (c : α) (h : disjoint a b) :
disjoint a (c b)
structure is_compl {α : Type u} [bounded_lattice α] (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} [bounded_lattice α] {x y : α} (h : is_compl x y) :
theorem is_compl.symm {α : Type u} [bounded_lattice α] {x y : α} (h : is_compl x y) :
theorem is_compl.of_eq {α : Type u} [bounded_lattice α] {x y : α} (h₁ : x y = ) (h₂ : x y = ) :
theorem is_compl.inf_eq_bot {α : Type u} [bounded_lattice α] {x y : α} (h : is_compl x y) :
x y =
theorem is_compl.sup_eq_top {α : Type u} [bounded_lattice α] {x y : α} (h : is_compl x y) :
x y =
theorem is_compl.inf_left_eq_bot_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} (h : is_compl y z) :
x y = x z
theorem is_compl.inf_right_eq_bot_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} (h : is_compl y z) :
x z = x y
theorem is_compl.disjoint_left_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} (h : is_compl y z) :
disjoint x y x z
theorem is_compl.disjoint_right_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} (h : is_compl y z) :
disjoint x z x y
theorem is_compl.le_left_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} (h : is_compl x y) :
z x disjoint z y
theorem is_compl.le_right_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} (h : is_compl x y) :
z y disjoint z x
theorem is_compl.left_le_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} (h : is_compl x y) :
x z z y
theorem is_compl.right_le_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} (h : is_compl x y) :
y z z x
theorem is_compl.antitone {α : Type u} [bounded_distrib_lattice α] {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} [bounded_distrib_lattice α] {x y z : α} (hxy : is_compl x y) (hxz : is_compl x z) :
y = z
theorem is_compl.left_unique {α : Type u} [bounded_distrib_lattice α] {x y z : α} (hxz : is_compl x z) (hyz : is_compl y z) :
x = y
theorem is_compl.sup_inf {α : Type u} [bounded_distrib_lattice α] {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} [bounded_distrib_lattice α] {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} [bounded_lattice α] :
theorem is_compl_top_bot {α : Type u} [bounded_lattice α] :
theorem eq_top_of_is_compl_bot {α : Type u} [bounded_lattice α] {x : α} (h : is_compl x ) :
x =
theorem eq_top_of_bot_is_compl {α : Type u} [bounded_lattice α] {x : α} (h : is_compl x) :
x =
theorem eq_bot_of_is_compl_top {α : Type u} [bounded_lattice α] {x : α} (h : is_compl x ) :
x =
theorem eq_bot_of_top_is_compl {α : Type u} [bounded_lattice α] {x : α} (h : is_compl x) :
x =
@[class]
structure is_complemented (α : Type u_1) [bounded_lattice α] :
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
theorem bot_ne_top {α : Type u} [bounded_lattice α] [nontrivial α] :
theorem top_ne_bot {α : Type u} [bounded_lattice α] [nontrivial α] :
@[instance]
Equations
@[simp]
theorem top_eq_tt  :
@[simp]
theorem bot_eq_ff  :