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 #

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

Typeclass for the ⊤ (\top) notation

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

Typeclass for the ⊥ (\bot) notation

Instances
source
@[protected, instance]
def has_top_nonempty (α : Type u) [has_top α] :
nonempty α
source
@[protected, instance]
def has_bot_nonempty (α : Type u) [has_bot α] :
nonempty α
source
@[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
source
@[instance]
def order_top.to_has_top (α : Type u) [has_le α] [self : order_top α] :
has_top α
source
@[simp]
theorem le_top {α : Type u} [has_le α] [order_top α] {a : α} :
a ≤ ⊤
source
@[simp]
theorem not_top_lt {α : Type u} [preorder α] [order_top α] {a : α} :
¬⊤ < a
source
theorem top_unique {α : Type u} [partial_order α] [order_top α] {a : α} (h : ⊤ ≤ a) :
a = ⊤
source
theorem eq_top_iff {α : Type u} [partial_order α] [order_top α] {a : α} :
a = ⊤ ↔ ⊤ ≤ a
source
@[simp]
theorem top_le_iff {α : Type u} [partial_order α] [order_top α] {a : α} :
⊤ ≤ a ↔ a = ⊤
source
@[simp]
theorem is_top_iff_eq_top {α : Type u} [partial_order α] [order_top α] {a : α} :
is_top a ↔ a = ⊤
source
theorem eq_top_mono {α : Type u} [partial_order α] [order_top α] {a b : α} (h : a ≤ b) (h₂ : a = ⊤) :
b = ⊤
source
theorem lt_top_iff_ne_top {α : Type u} [partial_order α] [order_top α] {a : α} :
a < ⊤ ↔ a ≠ ⊤
source
theorem eq_top_or_lt_top {α : Type u} [partial_order α] [order_top α] (a : α) :
a = ⊤ ∨ a < ⊤
source
theorem ne_top_of_lt {α : Type u} [partial_order α] [order_top α] {a b : α} (h : a < b) :
a ≠ ⊤
source
theorem has_lt.lt.ne_top {α : Type u} [partial_order α] [order_top α] {a b : α} (h : a < b) :
a ≠ ⊤

Alias of ne_top_of_lt.

source
theorem ne_top_of_le_ne_top {α : Type u} [partial_order α] [order_top α] {a b : α} (hb : b ≠ ⊤) (hab : a ≤ b) :
a ≠ ⊤
source
theorem eq_top_of_maximal {α : Type u} [partial_order α] [order_top α] {a : α} (h : ∀ (b : α), ¬a < b) :
a = ⊤
source
theorem ne.lt_top {α : Type u} [partial_order α] [order_top α] {a : α} (h : a ≠ ⊤) :
a < ⊤
source
theorem ne.lt_top' {α : Type u} [partial_order α] [order_top α] {a : α} (h : ⊤ ≠ a) :
a < ⊤
source
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
source
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) :
⊤ = ⊤
source
theorem order_top.ext {α : Type u_1} [partial_order α] {A B : order_top α} :
A = B
source
@[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
source
@[instance]
def order_bot.to_has_bot (α : Type u) [has_le α] [self : order_bot α] :
has_bot α
source
@[simp]
theorem bot_le {α : Type u} [has_le α] [order_bot α] {a : α} :
⊥ ≤ a
source
@[simp]
theorem not_lt_bot {α : Type u} [preorder α] [order_bot α] {a : α} :
¬a < ⊥
source
theorem bot_unique {α : Type u} [partial_order α] [order_bot α] {a : α} (h : a ≤ ⊥) :
a = ⊥
source
theorem eq_bot_iff {α : Type u} [partial_order α] [order_bot α] {a : α} :
a = ⊥ ↔ a ≤ ⊥
source
@[simp]
theorem le_bot_iff {α : Type u} [partial_order α] [order_bot α] {a : α} :
a ≤ ⊥ ↔ a = ⊥
source
@[simp]
theorem is_bot_iff_eq_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :
is_bot a ↔ a = ⊥
source
theorem ne_bot_of_le_ne_bot {α : Type u} [partial_order α] [order_bot α] {a b : α} (hb : b ≠ ⊥) (hab : b ≤ a) :
a ≠ ⊥
source
theorem eq_bot_mono {α : Type u} [partial_order α] [order_bot α] {a b : α} (h : a ≤ b) (h₂ : b = ⊥) :
a = ⊥
source
theorem bot_lt_iff_ne_bot {α : Type u} [partial_order α] [order_bot α] {a : α} :
⊥ < a ↔ a ≠ ⊥
source
theorem eq_bot_or_bot_lt {α : Type u} [partial_order α] [order_bot α] (a : α) :
a = ⊥ ∨ ⊥ < a
source
theorem ne_bot_of_gt {α : Type u} [partial_order α] [order_bot α] {a b : α} (h : a < b) :
b ≠ ⊥
source
theorem has_lt.lt.ne_bot {α : Type u} [partial_order α] [order_bot α] {a b : α} (h : a < b) :
b ≠ ⊥

Alias of ne_bot_of_gt.

source
theorem eq_bot_of_minimal {α : Type u} [partial_order α] [order_bot α] {a : α} (h : ∀ (b : α), ¬b < a) :
a = ⊥
source
theorem ne.bot_lt {α : Type u} [partial_order α] [order_bot α] {a : α} (h : a ≠ ⊥) :
⊥ < a
source
theorem ne.bot_lt' {α : Type u} [partial_order α] [order_bot α] {a : α} (h : ⊥ ≠ a) :
⊥ < a
source
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
source
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) :
⊥ = ⊥
source
theorem order_bot.ext {α : Type u_1} [partial_order α] {A B : order_bot α} :
A = B
source
@[simp]
theorem top_sup_eq {α : Type u} [semilattice_sup α] [order_top α] {a : α} :
⊤ ⊔ a = ⊤
source
@[simp]
theorem sup_top_eq {α : Type u} [semilattice_sup α] [order_top α] {a : α} :
a ⊔ ⊤ = ⊤
source
@[simp]
theorem bot_sup_eq {α : Type u} [semilattice_sup α] [order_bot α] {a : α} :
⊥ ⊔ a = a
source
@[simp]
theorem sup_bot_eq {α : Type u} [semilattice_sup α] [order_bot α] {a : α} :
a ⊔ ⊥ = a
source
@[simp]
theorem sup_eq_bot_iff {α : Type u} [semilattice_sup α] [order_bot α] {a b : α} :
a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
source
@[simp]
theorem top_inf_eq {α : Type u} [semilattice_inf α] [order_top α] {a : α} :
⊤ ⊓ a = a
source
@[simp]
theorem inf_top_eq {α : Type u} [semilattice_inf α] [order_top α] {a : α} :
a ⊓ ⊤ = a
source
@[simp]
theorem inf_eq_top_iff {α : Type u} [semilattice_inf α] [order_top α] {a b : α} :
a ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤
source
@[simp]
theorem bot_inf_eq {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :
⊥ ⊓ a = ⊥
source
@[simp]
theorem inf_bot_eq {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :
a ⊓ ⊥ = ⊥

Bounded order #

source
@[instance]
def bounded_order.to_order_bot (α : Type u) [has_le α] [self : bounded_order α] :
order_bot α
source
@[instance]
def bounded_order.to_order_top (α : Type u) [has_le α] [self : bounded_order α] :
order_top α
source
@[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
source
theorem bounded_order.ext {α : Type u_1} [partial_order α] {A B : bounded_order α} :
A = B
source
@[protected, instance]
def Prop.distrib_lattice  :
distrib_lattice Prop

Propositions form a distributive lattice.

Equations
source
@[protected, instance]
def Prop.bounded_order  :
bounded_order Prop

Propositions form a bounded order.

Equations
source
@[protected, instance]
noncomputable def Prop.linear_order  :
linear_order Prop
Equations
source
@[simp]
theorem le_Prop_eq  :
has_le.le = λ (_x _y : Prop), _x → _y
source
@[simp]
theorem sup_Prop_eq  :
has_sup.sup = or
source
@[simp]
theorem inf_Prop_eq  :
has_inf.inf = and
source
theorem monotone_and {α : Type u} [preorder α] {p q : α → Prop} (m_p : monotone p) (m_q : monotone q) :
monotone (λ (x : α), p x ∧ q x)
source
theorem monotone_or {α : Type u} [preorder α] {p q : α → Prop} (m_p : monotone p) (m_q : monotone q) :
monotone (λ (x : α), p x ∨ q x)

Function lattices #

source
@[protected, instance]
def pi.has_bot {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_bot (α' i)] :
has_bot (Π (i : ι), α' i)
Equations
source
@[simp]
theorem pi.bot_apply {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_bot (α' i)] (i : ι) :
⊥ i = ⊥
source
theorem pi.bot_def {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_bot (α' i)] :
⊥ = λ (i : ι), ⊥
source
@[protected, instance]
def pi.has_top {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_top (α' i)] :
has_top (Π (i : ι), α' i)
Equations
source
@[simp]
theorem pi.top_apply {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_top (α' i)] (i : ι) :
⊤ i = ⊤
source
theorem pi.top_def {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_top (α' i)] :
⊤ = λ (i : ι), ⊤
source
@[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
source
@[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
source
@[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
source
theorem eq_bot_of_bot_eq_top {α : Type u} [partial_order α] [bounded_order α] (hα : ⊥ = ⊤) (x : α) :
x = ⊥
source
theorem eq_top_of_bot_eq_top {α : Type u} [partial_order α] [bounded_order α] (hα : ⊥ = ⊤) (x : α) :
x = ⊤
source
theorem subsingleton_of_top_le_bot {α : Type u} [partial_order α] [bounded_order α] (h : ⊤ ≤ ⊥) :
subsingleton α
source
theorem subsingleton_of_bot_eq_top {α : Type u} [partial_order α] [bounded_order α] (hα : ⊥ = ⊤) :
subsingleton α
source
theorem subsingleton_iff_bot_eq_top {α : Type u} [partial_order α] [bounded_order α] :
⊥ = ⊤ ↔ subsingleton α

with_bot, with_top #

source
def with_bot (α : Type u_1) :
Type u_1

Attach ⊥ to a type.

Equations
source
@[protected, instance]
meta def with_bot.has_to_format {α : Type u_1} [has_to_format α] :
has_to_format (with_bot α)
source
@[protected, instance]
def with_bot.has_coe_t {α : Type u} :
has_coe_t α (with_bot α)
Equations
source
@[protected, instance]
def with_bot.has_bot {α : Type u} :
has_bot (with_bot α)
Equations
source
@[protected, instance]
def with_bot.inhabited {α : Type u} :
inhabited (with_bot α)
Equations
source
theorem with_bot.none_eq_bot {α : Type u} :
none = ⊥
source
theorem with_bot.some_eq_coe {α : Type u} (a : α) :
some a = ↑a
source
@[simp]
theorem with_bot.bot_ne_coe {α : Type u} (a : α) :
⊥ ≠ ↑a
source
@[simp]
theorem with_bot.coe_ne_bot {α : Type u} (a : α) :
↑a ≠ ⊥
source
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
source
@[norm_cast]
theorem with_bot.coe_eq_coe {α : Type u} {a b : α} :
↑a = ↑b ↔ a = b
source
theorem with_bot.ne_bot_iff_exists {α : Type u} {x : with_bot α} :
x ≠ ⊥ ↔ ∃ (a : α), ↑a = x
source
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
source
@[simp]
theorem with_bot.coe_unbot {α : Type u_1} (x : with_bot α) (h : x ≠ ⊥) :
↑(x.unbot h) = x
source
@[simp]
theorem with_bot.unbot_coe {α : Type u} (x : α) (h : ↑x ≠ ⊥ := _) :
↑x.unbot h = x
source
@[protected, instance]
def with_bot.has_le {α : Type u} [has_le α] :
has_le (with_bot α)
Equations
source
@[protected, instance]
def with_bot.has_lt {α : Type u} [has_lt α] :
has_lt (with_bot α)
Equations
source
@[simp]
theorem with_bot.some_lt_some {α : Type u} [has_lt α] {a b : α} :
some a < some b ↔ a < b
source
theorem with_bot.none_lt_some {α : Type u} [has_lt α] (a : α) :
none < some a
source
theorem with_bot.not_lt_none {α : Type u} [has_lt α] (a : option α) :
¬a < none
source
theorem with_bot.bot_lt_coe {α : Type u} [has_lt α] (a : α) :
⊥ < ↑a
source
@[protected, instance]
def with_bot.can_lift {α : Type u} :
can_lift (with_bot α) α
Equations
source
@[protected, instance]
def with_bot.preorder {α : Type u} [preorder α] :
preorder (with_bot α)
Equations
source
@[protected, instance]
def with_bot.partial_order {α : Type u} [partial_order α] :
partial_order (with_bot α)
Equations
source
@[protected, instance]
def with_bot.order_bot {α : Type u} [has_le α] :
order_bot (with_bot α)
Equations
source
@[simp, norm_cast]
theorem with_bot.coe_le_coe {α : Type u} [has_le α] {a b : α} :
↑a ≤ ↑b ↔ a ≤ b
source
@[simp]
theorem with_bot.some_le_some {α : Type u} [has_le α] {a b : α} :
some a ≤ some b ↔ a ≤ b
source
theorem with_bot.coe_le {α : Type u} [has_le α] {a b : α} {o : option α} :
b ∈ o → (↑a ≤ o ↔ a ≤ b)
source
@[norm_cast]
theorem with_bot.coe_lt_coe {α : Type u} [has_lt α] {a b : α} :
↑a < ↑b ↔ a < b
source
theorem with_bot.le_coe_get_or_else {α : Type u} [preorder α] (a : with_bot α) (b : α) :
a ≤ ↑(option.get_or_else a b)
source
@[simp]
theorem with_bot.get_or_else_bot {α : Type u} (a : α) :
option.get_or_else ⊥ a = a
source
theorem with_bot.get_or_else_bot_le_iff {α : Type u} [has_le α] [order_bot α] {a : with_bot α} {b : α} :
option.get_or_else a ⊥ ≤ b ↔ a ≤ ↑b
source
@[protected, instance]
def with_bot.decidable_le {α : Type u} [has_le α] [decidable_rel has_le.le] :
decidable_rel has_le.le
Equations
source
@[protected, instance]
def with_bot.decidable_lt {α : Type u} [has_lt α] [decidable_rel has_lt.lt] :
decidable_rel has_lt.lt
Equations
source
@[protected, instance]
def with_bot.has_le.le.is_total {α : Type u} [partial_order α] [is_total α has_le.le] :
is_total (with_bot α) has_le.le
source
@[protected, instance]
def with_bot.semilattice_sup {α : Type u} [semilattice_sup α] :
semilattice_sup (with_bot α)
Equations
source
theorem with_bot.coe_sup {α : Type u} [semilattice_sup α] (a b : α) :
↑(a ⊔ b) = ↑a ⊔ ↑b
source
@[protected, instance]
def with_bot.semilattice_inf {α : Type u} [semilattice_inf α] :
semilattice_inf (with_bot α)
Equations
source
theorem with_bot.coe_inf {α : Type u} [semilattice_inf α] (a b : α) :
↑(a ⊓ b) = ↑a ⊓ ↑b
source
@[protected, instance]
def with_bot.lattice {α : Type u} [lattice α] :
lattice (with_bot α)
Equations
source
@[protected, instance]
def with_bot.linear_order {α : Type u} [linear_order α] :
linear_order (with_bot α)
Equations
source
@[norm_cast]
theorem with_bot.coe_min {α : Type u} [linear_order α] (x y : α) :
↑(min x y) = min ↑x ↑y
source
@[norm_cast]
theorem with_bot.coe_max {α : Type u} [linear_order α] (x y : α) :
↑(max x y) = max ↑x ↑y
source
@[protected, instance]
def with_bot.order_top {α : Type u} [has_le α] [order_top α] :
order_top (with_bot α)
Equations
source
@[protected, instance]
def with_bot.bounded_order {α : Type u} [has_le α] [order_top α] :
bounded_order (with_bot α)
Equations
source
theorem with_bot.well_founded_lt {α : Type u} [preorder α] (h : well_founded has_lt.lt) :
well_founded has_lt.lt
source
@[protected, instance]
def with_bot.densely_ordered {α : Type u} [has_lt α] [densely_ordered α] [no_bot_order α] :
densely_ordered (with_bot α)
source
@[protected, instance]
def with_bot.no_top_order {α : Type u_1} [has_lt α] [no_top_order α] [nonempty α] :
no_top_order (with_bot α)
source
def with_top (α : Type u_1) :
Type u_1

Attach ⊤ to a type.

Equations
source
@[protected, instance]
meta def with_top.has_to_format {α : Type u_1} [has_to_format α] :
has_to_format (with_top α)
source
@[protected, instance]
def with_top.has_coe_t {α : Type u} :
has_coe_t α (with_top α)
Equations
source
@[protected, instance]
def with_top.has_top {α : Type u} :
has_top (with_top α)
Equations
source
@[protected, instance]
def with_top.inhabited {α : Type u} :
inhabited (with_top α)
Equations
source
theorem with_top.none_eq_top {α : Type u} :
none = ⊤
source
theorem with_top.some_eq_coe {α : Type u} (a : α) :
some a = ↑a
source
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
source
@[norm_cast]
theorem with_top.coe_eq_coe {α : Type u} {a b : α} :
↑a = ↑b ↔ a = b
source
@[simp]
theorem with_top.top_ne_coe {α : Type u} {a : α} :
⊤ ≠ ↑a
source
@[simp]
theorem with_top.coe_ne_top {α : Type u} {a : α} :
↑a ≠ ⊤
source
theorem with_top.ne_top_iff_exists {α : Type u} {x : with_top α} :
x ≠ ⊤ ↔ ∃ (a : α), ↑a = x
source
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
source
@[simp]
theorem with_top.coe_untop {α : Type u_1} (x : with_top α) (h : x ≠ ⊤) :
↑(x.untop h) = x
source
@[simp]
theorem with_top.untop_coe {α : Type u} (x : α) (h : ↑x ≠ ⊤ := with_top.coe_ne_top) :
↑x.untop h = x
source
@[protected, instance]
def with_top.has_lt {α : Type u} [has_lt α] :
has_lt (with_top α)
Equations
source
@[protected, instance]
def with_top.has_le {α : Type u} [has_le α] :
has_le (with_top α)
Equations
source
@[simp]
theorem with_top.some_lt_some {α : Type u} [has_lt α] {a b : α} :
some a < some b ↔ a < b
source
@[simp]
theorem with_top.some_le_some {α : Type u} [has_le α] {a b : α} :
some a ≤ some b ↔ a ≤ b
source
@[simp]
theorem with_top.le_none {α : Type u} [has_le α] {a : with_top α} :
a ≤ none
source
@[simp]
theorem with_top.some_lt_none {α : Type u} [has_lt α] (a : α) :
some a < none
source
@[simp]
theorem with_top.not_none_lt {α : Type u} [has_lt α] (a : option α) :
¬none < a
source
@[protected, instance]
def with_top.can_lift {α : Type u} :
can_lift (with_top α) α
Equations
source
@[protected, instance]
def with_top.preorder {α : Type u} [preorder α] :
preorder (with_top α)
Equations
source
@[protected, instance]
def with_top.partial_order {α : Type u} [partial_order α] :
partial_order (with_top α)
Equations
source
@[protected, instance]
def with_top.order_top {α : Type u} [has_le α] :
order_top (with_top α)
Equations
source
@[simp, norm_cast]
theorem with_top.coe_le_coe {α : Type u} [has_le α] {a b : α} :
↑a ≤ ↑b ↔ a ≤ b
source
theorem with_top.le_coe {α : Type u} [has_le α] {a b : α} {o : option α} :
a ∈ o → (o ≤ ↑b ↔ a ≤ b)
source
theorem with_top.le_coe_iff {α : Type u} [partial_order α] {b : α} {x : with_top α} :
x ≤ ↑b ↔ ∃ (a : α), x = ↑a ∧ a ≤ b
source
theorem with_top.coe_le_iff {α : Type u} [partial_order α] {a : α} {x : with_top α} :
↑a ≤ x ↔ ∀ (b : α), x = ↑b → a ≤ b
source
theorem with_top.lt_iff_exists_coe {α : Type u} [partial_order α] {a b : with_top α} :
a < b ↔ ∃ (p : α), a = ↑p ∧ ↑p < b
source
@[norm_cast]
theorem with_top.coe_lt_coe {α : Type u} [has_lt α] {a b : α} :
↑a < ↑b ↔ a < b
source
theorem with_top.coe_lt_top {α : Type u} [has_lt α] (a : α) :
↑a < ⊤
source
theorem with_top.coe_lt_iff {α : Type u} [preorder α] {a : α} {x : with_top α} :
↑a < x ↔ ∀ (b : α), x = ↑b → a < b
source
theorem with_top.not_top_le_coe {α : Type u} [preorder α] (a : α) :
¬⊤ ≤ ↑a
source
@[protected, instance]
def with_top.decidable_le {α : Type u} [has_le α] [decidable_rel has_le.le] :
decidable_rel has_le.le
Equations
source
@[protected, instance]
def with_top.decidable_lt {α : Type u} [has_lt α] [decidable_rel has_lt.lt] :
decidable_rel has_lt.lt
Equations
source
@[protected, instance]
def with_top.has_le.le.is_total {α : Type u} [partial_order α] [is_total α has_le.le] :
is_total (with_top α) has_le.le
source
@[protected, instance]
def with_top.semilattice_inf {α : Type u} [semilattice_inf α] :
semilattice_inf (with_top α)
Equations
source
theorem with_top.coe_inf {α : Type u} [semilattice_inf α] (a b : α) :
↑(a ⊓ b) = ↑a ⊓ ↑b
source
@[protected, instance]
def with_top.semilattice_sup {α : Type u} [semilattice_sup α] :
semilattice_sup (with_top α)
Equations
source
theorem with_top.coe_sup {α : Type u} [semilattice_sup α] (a b : α) :
↑(a ⊔ b) = ↑a ⊔ ↑b
source
@[protected, instance]
def with_top.lattice {α : Type u} [lattice α] :
lattice (with_top α)
Equations
source
@[protected, instance]
def with_top.linear_order {α : Type u} [linear_order α] :
linear_order (with_top α)
Equations
source
@[simp, norm_cast]
theorem with_top.coe_min {α : Type u} [linear_order α] (x y : α) :
↑(min x y) = min ↑x ↑y
source
@[simp, norm_cast]
theorem with_top.coe_max {α : Type u} [linear_order α] (x y : α) :
↑(max x y) = max ↑x ↑y
source
@[protected, instance]
def with_top.order_bot {α : Type u} [has_le α] [order_bot α] :
order_bot (with_top α)
Equations
source
@[protected, instance]
def with_top.bounded_order {α : Type u} [has_le α] [order_bot α] :
bounded_order (with_top α)
Equations
source
theorem with_top.well_founded_lt {α : Type u_1} [preorder α] (h : well_founded has_lt.lt) :
well_founded has_lt.lt
source
@[protected, instance]
def with_top.densely_ordered {α : Type u} [has_lt α] [densely_ordered α] [no_top_order α] :
densely_ordered (with_top α)
source
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
source
@[protected, instance]
def with_top.no_bot_order {α : Type u_1} [has_lt α] [no_bot_order α] [nonempty α] :
no_bot_order (with_top α)

Subtype, order dual, product lattices #

source
@[protected]
def subtype.order_bot {α : Type u} [preorder α] [order_bot α] {P : α → Prop} (Pbot : P ⊥) :
order_bot {x // P x}

A subtype remains a ⊥-order if the property holds at ⊥. See note [reducible non-instances].

Equations
source
@[protected]
def subtype.order_top {α : Type u} [preorder α] [order_top α] {P : α → Prop} (Ptop : P ⊤) :
order_top {x // P x}

A subtype remains a ⊤-order if the property holds at ⊤. See note [reducible non-instances].

Equations
source
@[protected, instance]
def order_dual.has_top (α : Type u) [has_bot α] :
has_top (order_dual α)
Equations
source
@[protected, instance]
def order_dual.has_bot (α : Type u) [has_top α] :
has_bot (order_dual α)
Equations
source
@[protected, instance]
def order_dual.order_top (α : Type u) [has_le α] [order_bot α] :
order_top (order_dual α)
Equations
source
@[protected, instance]
def order_dual.order_bot (α : Type u) [has_le α] [order_top α] :
order_bot (order_dual α)
Equations
source
@[protected, instance]
def order_dual.bounded_order (α : Type u) [has_le α] [bounded_order α] :
bounded_order (order_dual α)
Equations
source
@[protected, instance]
def prod.has_top (α : Type u) (β : Type v) [has_top α] [has_top β] :
has_top (α × β)
Equations
source
@[protected, instance]
def prod.has_bot (α : Type u) (β : Type v) [has_bot α] [has_bot β] :
has_bot (α × β)
Equations
source
@[protected, instance]
def prod.order_top (α : Type u) (β : Type v) [has_le α] [has_le β] [order_top α] [order_top β] :
order_top (α × β)
Equations
source
@[protected, instance]
def prod.order_bot (α : Type u) (β : Type v) [has_le α] [has_le β] [order_bot α] [order_bot β] :
order_bot (α × β)
Equations
source
@[protected, instance]
def prod.bounded_order (α : Type u) (β : Type v) [has_le α] [has_le β] [bounded_order α] [bounded_order β] :
bounded_order (α × β)
Equations

Disjointness and complements #

source
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
source
theorem disjoint.eq_bot {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (h : disjoint a b) :
a ⊓ b = ⊥
source
theorem disjoint_iff {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} :
disjoint a b ↔ a ⊓ b = ⊥
source
theorem disjoint.comm {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} :
disjoint a b ↔ disjoint b a
source
theorem disjoint.symm {α : Type u} [semilattice_inf α] [order_bot α] ⦃a b : α⦄ :
disjoint a b → disjoint b a
source
theorem symmetric_disjoint {α : Type u} [semilattice_inf α] [order_bot α] :
symmetric disjoint
source
@[simp]
theorem disjoint_bot_left {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :
disjoint ⊥ a
source
@[simp]
theorem disjoint_bot_right {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :
disjoint a ⊥
source
theorem disjoint.mono {α : Type u} [semilattice_inf α] [order_bot α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
disjoint b d → disjoint a c
source
theorem disjoint.mono_left {α : Type u} [semilattice_inf α] [order_bot α] {a b c : α} (h : a ≤ b) :
disjoint b c → disjoint a c
source
theorem disjoint.mono_right {α : Type u} [semilattice_inf α] [order_bot α] {a b c : α} (h : b ≤ c) :
disjoint a c → disjoint a b
source
@[simp]
theorem disjoint_self {α : Type u} [semilattice_inf α] [order_bot α] {a : α} :
disjoint a a ↔ a = ⊥
source
theorem disjoint.ne {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (ha : a ≠ ⊥) (hab : disjoint a b) :
a ≠ b
source
theorem disjoint.eq_bot_of_le {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (hab : disjoint a b) (h : a ≤ b) :
a = ⊥
source
theorem disjoint.of_disjoint_inf_of_le {α : Type u} [semilattice_inf α] [order_bot α] {a b c : α} (h : disjoint (a ⊓ b) c) (hle : a ≤ c) :
disjoint a b
source
theorem disjoint.of_disjoint_inf_of_le' {α : Type u} [semilattice_inf α] [order_bot α] {a b c : α} (h : disjoint (a ⊓ b) c) (hle : b ≤ c) :
disjoint a b
source
@[simp]
theorem disjoint_top {α : Type u} [lattice α] [bounded_order α] {a : α} :
disjoint a ⊤ ↔ a = ⊥
source
@[simp]
theorem top_disjoint {α : Type u} [lattice α] [bounded_order α] {a : α} :
disjoint ⊤ a ↔ a = ⊥
source
theorem eq_bot_of_disjoint_absorbs {α : Type u} [lattice α] [bounded_order α] {a b : α} (w : disjoint a b) (h : a ⊔ b = a) :
b = ⊥
source
theorem min_top_left {α : Type u} [linear_order α] [order_top α] (a : α) :
min ⊤ a = a
source
theorem min_top_right {α : Type u} [linear_order α] [order_top α] (a : α) :
min a ⊤ = a
source
theorem max_bot_left {α : Type u} [linear_order α] [order_bot α] (a : α) :
max ⊥ a = a
source
theorem max_bot_right {α : Type u} [linear_order α] [order_bot α] (a : α) :
max a ⊥ = a
source
theorem min_bot_left {α : Type u} [linear_order α] [order_bot α] (a : α) :
min ⊥ a = ⊥
source
theorem min_bot_right {α : Type u} [linear_order α] [order_bot α] (a : α) :
min a ⊥ = ⊥
source
theorem max_top_left {α : Type u} [linear_order α] [order_top α] (a : α) :
max ⊤ a = ⊤
source
theorem max_top_right {α : Type u} [linear_order α] [order_top α] (a : α) :
max a ⊤ = ⊤
source
@[simp]
theorem min_eq_bot {α : Type u} [linear_order α] [order_bot α] {a b : α} :
min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥
source
@[simp]
theorem max_eq_top {α : Type u} [linear_order α] [order_top α] {a b : α} :
max a b = ⊤ ↔ a = ⊤ ∨ b = ⊤
source
@[simp]
theorem max_eq_bot {α : Type u} [linear_order α] [order_bot α] {a b : α} :
max a b = ⊥ ↔ a = ⊥ ∧ b = ⊥
source
@[simp]
theorem min_eq_top {α : Type u} [linear_order α] [order_top α] {a b : α} :
min a b = ⊤ ↔ a = ⊤ ∧ b = ⊤
source
@[simp]
theorem disjoint_sup_left {α : Type u} [distrib_lattice α] [order_bot α] {a b c : α} :
disjoint (a ⊔ b) c ↔ disjoint a c ∧ disjoint b c
source
@[simp]
theorem disjoint_sup_right {α : Type u} [distrib_lattice α] [order_bot α] {a b c : α} :
disjoint a (b ⊔ c) ↔ disjoint a b ∧ disjoint a c
source
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
source
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)
source
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
source
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
source
theorem disjoint.inf_left {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (c : α) (h : disjoint a b) :
disjoint (a ⊓ c) b
source
theorem disjoint.inf_left' {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (c : α) (h : disjoint a b) :
disjoint (c ⊓ a) b
source
theorem disjoint.inf_right {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (c : α) (h : disjoint a b) :
disjoint a (b ⊓ c)
source
theorem disjoint.inf_right' {α : Type u} [semilattice_inf α] [order_bot α] {a b : α} (c : α) (h : disjoint a b) :
disjoint a (c ⊓ b)
source
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
source
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 = ⊥.

source
@[protected]
theorem is_compl.disjoint {α : Type u} [lattice α] [bounded_order α] {x y : α} (h : is_compl x y) :
disjoint x y
source
@[protected]
theorem is_compl.symm {α : Type u} [lattice α] [bounded_order α] {x y : α} (h : is_compl x y) :
is_compl y x
source
theorem is_compl.of_eq {α : Type u} [lattice α] [bounded_order α] {x y : α} (h₁ : x ⊓ y = ⊥) (h₂ : x ⊔ y = ⊤) :
is_compl x y
source
theorem is_compl.inf_eq_bot {α : Type u} [lattice α] [bounded_order α] {x y : α} (h : is_compl x y) :
x ⊓ y = ⊥
source
theorem is_compl.sup_eq_top {α : Type u} [lattice α] [bounded_order α] {x y : α} (h : is_compl x y) :
x ⊔ y = ⊤
source
theorem is_compl.to_order_dual {α : Type u} [lattice α] [bounded_order α] {x y : α} (h : is_compl x y) :
is_compl (⇑order_dual.to_dual x) (⇑order_dual.to_dual y)
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem is_compl.left_le_iff {α : Type u} [distrib_lattice α] [bounded_order α] {x y z : α} (h : is_compl x y) :
x ≤ z ↔ ⊤ ≤ z ⊔ y
source
theorem is_compl.right_le_iff {α : Type u} [distrib_lattice α] [bounded_order α] {x y z : α} (h : is_compl x y) :
y ≤ z ↔ ⊤ ≤ z ⊔ x
source
@[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
source
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
source
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
source
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')
source
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')
source
theorem is_compl_bot_top {α : Type u} [lattice α] [bounded_order α] :
is_compl ⊥ ⊤
source
theorem is_compl_top_bot {α : Type u} [lattice α] [bounded_order α] :
is_compl ⊤ ⊥
source
theorem eq_top_of_is_compl_bot {α : Type u} [lattice α] [bounded_order α] {x : α} (h : is_compl x ⊥) :
x = ⊤
source
theorem eq_top_of_bot_is_compl {α : Type u} [lattice α] [bounded_order α] {x : α} (h : is_compl ⊥ x) :
x = ⊤
source
theorem eq_bot_of_is_compl_top {α : Type u} [lattice α] [bounded_order α] {x : α} (h : is_compl x ⊤) :
x = ⊥
source
theorem eq_bot_of_top_is_compl {α : Type u} [lattice α] [bounded_order α] {x : α} (h : is_compl ⊤ x) :
x = ⊥
source
@[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
source
@[protected, instance]
def is_complemented.order_dual.is_complemented {α : Type u} [lattice α] [bounded_order α] [is_complemented α] :
is_complemented (order_dual α)
source
theorem bot_ne_top {α : Type u} [partial_order α] [bounded_order α] [nontrivial α] :
⊥ ≠ ⊤
source
theorem top_ne_bot {α : Type u} [partial_order α] [bounded_order α] [nontrivial α] :
⊤ ≠ ⊥
source
@[protected, instance]
def bool.bounded_order  :
bounded_order bool
Equations
source
@[simp]
theorem top_eq_tt  :
⊤ = tt
source
@[simp]
theorem bot_eq_ff  :
⊥ = ff