mathlib documentation

order.bounded_lattice

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
@[class]
structure order_top (α : Type u) :
Type u
  • top : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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
source
@[instance]
def order_top.to_partial_order (α : Type u) [self : order_top α] :
partial_order α
source
@[instance]
def order_top.to_has_top (α : Type u) [self : order_top α] :
has_top α
source
@[simp]
theorem le_top {α : Type u} [order_top α] {a : α} :
a ≤ ⊤
source
theorem top_unique {α : Type u} [order_top α] {a : α} (h : ⊤ ≤ a) :
a = ⊤
source
theorem eq_top_iff {α : Type u} [order_top α] {a : α} :
a = ⊤ ↔ ⊤ ≤ a
source
@[simp]
theorem top_le_iff {α : Type u} [order_top α] {a : α} :
⊤ ≤ a ↔ a = ⊤
source
@[simp]
theorem not_top_lt {α : Type u} [order_top α] {a : α} :
¬⊤ < a
source
theorem eq_top_mono {α : Type u} [order_top α] {a b : α} (h : a ≤ b) (h₂ : a = ⊤) :
b = ⊤
source
theorem lt_top_iff_ne_top {α : Type u} [order_top α] {a : α} :
a < ⊤ ↔ a ≠ ⊤
source
theorem ne_top_of_lt {α : Type u} [order_top α] {a b : α} (h : a < b) :
a ≠ ⊤
source
theorem ne_top_of_le_ne_top {α : Type u} [order_top α] {a b : α} (hb : b ≠ ⊤) (hab : a ≤ b) :
a ≠ ⊤
source
theorem eq_top_of_maximal {α : Type u} [order_top α] {a : α} (h : ∀ (b : α), ¬a < b) :
a = ⊤
source
theorem strict_mono.top_preimage_top' {α : Type u} {β : Type v} [linear_order α] [order_top β] {f : α → β} (H : strict_mono f) {a : α} (h_top : f a = ⊤) (x : α) :
x ≤ a
source
theorem order_top.ext_top {α : Type u_1} {A B : order_top α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :
⊤ = ⊤
source
theorem order_top.ext {α : Type u_1} {A B : order_top α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :
A = B
source
@[class]
structure order_bot (α : Type u) :
Type u
  • bot : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • bot_le : ∀ (a : α), ⊥ ≤ a

An order_bot is a partial order with a least element. (We could state this on preorders, but then it wouldn't be unique so distinguishing one would seem odd.)

Instances
source
@[instance]
def order_bot.to_partial_order (α : Type u) [self : order_bot α] :
partial_order α
source
@[instance]
def order_bot.to_has_bot (α : Type u) [self : order_bot α] :
has_bot α
source
@[simp]
theorem bot_le {α : Type u} [order_bot α] {a : α} :
⊥ ≤ a
source
theorem bot_unique {α : Type u} [order_bot α] {a : α} (h : a ≤ ⊥) :
a = ⊥
source
theorem eq_bot_iff {α : Type u} [order_bot α] {a : α} :
a = ⊥ ↔ a ≤ ⊥
source
@[simp]
theorem le_bot_iff {α : Type u} [order_bot α] {a : α} :
a ≤ ⊥ ↔ a = ⊥
source
@[simp]
theorem not_lt_bot {α : Type u} [order_bot α] {a : α} :
¬a < ⊥
source
theorem ne_bot_of_le_ne_bot {α : Type u} [order_bot α] {a b : α} (hb : b ≠ ⊥) (hab : b ≤ a) :
a ≠ ⊥
source
theorem eq_bot_mono {α : Type u} [order_bot α] {a b : α} (h : a ≤ b) (h₂ : b = ⊥) :
a = ⊥
source
theorem bot_lt_iff_ne_bot {α : Type u} [order_bot α] {a : α} :
⊥ < a ↔ a ≠ ⊥
source
theorem ne_bot_of_gt {α : Type u} [order_bot α] {a b : α} (h : a < b) :
b ≠ ⊥
source
theorem eq_bot_of_minimal {α : Type u} [order_bot α] {a : α} (h : ∀ (b : α), ¬b < a) :
a = ⊥
source
theorem strict_mono.bot_preimage_bot' {α : Type u} {β : Type v} [linear_order α] [order_bot β] {f : α → β} (H : strict_mono f) {a : α} (h_bot : f a = ⊥) (x : α) :
a ≤ x
source
theorem order_bot.ext_bot {α : Type u_1} {A B : order_bot α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :
⊥ = ⊥
source
theorem order_bot.ext {α : Type u_1} {A B : order_bot α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :
A = B
source
@[class]
structure semilattice_sup_top (α : Type u) :
Type u
  • top : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_top : ∀ (a : α), a ≤ ⊤
  • sup : α → α → α
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1

A semilattice_sup_top is a semilattice with top and join.

Instances
source
@[instance]
def semilattice_sup_top.to_order_top (α : Type u) [self : semilattice_sup_top α] :
order_top α
source
@[instance]
def semilattice_sup_top.to_semilattice_sup (α : Type u) [self : semilattice_sup_top α] :
semilattice_sup α
source
@[simp]
theorem top_sup_eq {α : Type u} [semilattice_sup_top α] {a : α} :
⊤ ⊔ a = ⊤
source
@[simp]
theorem sup_top_eq {α : Type u} [semilattice_sup_top α] {a : α} :
a ⊔ ⊤ = ⊤
source
@[instance]
def semilattice_sup_bot.to_order_bot (α : Type u) [self : semilattice_sup_bot α] :
order_bot α
source
@[instance]
def semilattice_sup_bot.to_semilattice_sup (α : Type u) [self : semilattice_sup_bot α] :
semilattice_sup α
source
@[class]
structure semilattice_sup_bot (α : Type u) :
Type u
  • bot : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • bot_le : ∀ (a : α), ⊥ ≤ a
  • sup : α → α → α
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1

A semilattice_sup_bot is a semilattice with bottom and join.

Instances
source
@[simp]
theorem bot_sup_eq {α : Type u} [semilattice_sup_bot α] {a : α} :
⊥ ⊔ a = a
source
@[simp]
theorem sup_bot_eq {α : Type u} [semilattice_sup_bot α] {a : α} :
a ⊔ ⊥ = a
source
@[simp]
theorem sup_eq_bot_iff {α : Type u} [semilattice_sup_bot α] {a b : α} :
a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
source
@[protected, instance]
def nat.semilattice_sup_bot  :
semilattice_sup_bot ℕ
Equations
source
@[class]
structure semilattice_inf_top (α : Type u) :
Type u
  • top : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_top : ∀ (a : α), a ≤ ⊤
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
  • inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
  • le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1

A semilattice_inf_top is a semilattice with top and meet.

Instances
source
@[instance]
def semilattice_inf_top.to_order_top (α : Type u) [self : semilattice_inf_top α] :
order_top α
source
@[instance]
def semilattice_inf_top.to_semilattice_inf (α : Type u) [self : semilattice_inf_top α] :
semilattice_inf α
source
@[simp]
theorem top_inf_eq {α : Type u} [semilattice_inf_top α] {a : α} :
⊤ ⊓ a = a
source
@[simp]
theorem inf_top_eq {α : Type u} [semilattice_inf_top α] {a : α} :
a ⊓ ⊤ = a
source
@[simp]
theorem inf_eq_top_iff {α : Type u} [semilattice_inf_top α] {a b : α} :
a ⊓ b = ⊤ ↔ a = ⊤ ∧ b = ⊤
source
@[instance]
def semilattice_inf_bot.to_order_bot (α : Type u) [self : semilattice_inf_bot α] :
order_bot α
source
@[class]
structure semilattice_inf_bot (α : Type u) :
Type u
  • bot : α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • bot_le : ∀ (a : α), ⊥ ≤ a
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
  • inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
  • le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1

A semilattice_inf_bot is a semilattice with bottom and meet.

Instances
source
@[instance]
def semilattice_inf_bot.to_semilattice_inf (α : Type u) [self : semilattice_inf_bot α] :
semilattice_inf α
source
@[simp]
theorem bot_inf_eq {α : Type u} [semilattice_inf_bot α] {a : α} :
⊥ ⊓ a = ⊥
source
@[simp]
theorem inf_bot_eq {α : Type u} [semilattice_inf_bot α] {a : α} :
a ⊓ ⊥ = ⊥
source
@[instance]
def bounded_lattice.to_order_top (α : Type u) [self : bounded_lattice α] :
order_top α
source
@[instance]
def bounded_lattice.to_order_bot (α : Type u) [self : bounded_lattice α] :
order_bot α
source
@[instance]
def bounded_lattice.to_lattice (α : Type u) [self : bounded_lattice α] :
lattice α
source
@[class]
structure bounded_lattice (α : Type u) :
Type u
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
  • inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
  • le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
  • top : α
  • le_top : ∀ (a : α), a ≤ ⊤
  • bot : α
  • bot_le : ∀ (a : α), ⊥ ≤ a

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

Instances
source
@[protected, instance]
def semilattice_inf_top_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :
semilattice_inf_top α
Equations
source
@[protected, instance]
def semilattice_inf_bot_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :
semilattice_inf_bot α
Equations
source
@[protected, instance]
def semilattice_sup_top_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :
semilattice_sup_top α
Equations
source
@[protected, instance]
def semilattice_sup_bot_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :
semilattice_sup_bot α
Equations
source
theorem bounded_lattice.ext {α : Type u_1} {A B : bounded_lattice α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :
A = B
source
@[instance]
def bounded_distrib_lattice.to_distrib_lattice (α : Type u_1) [self : bounded_distrib_lattice α] :
distrib_lattice α
source
@[class]
structure bounded_distrib_lattice (α : Type u_1) :
Type u_1
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
  • inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
  • le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
  • le_sup_inf : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
  • top : α
  • le_top : ∀ (a : α), a ≤ ⊤
  • bot : α
  • bot_le : ∀ (a : α), ⊥ ≤ a

A bounded distributive lattice is exactly what it sounds like.

Instances
source
@[instance]
def bounded_distrib_lattice.to_bounded_lattice (α : Type u_1) [self : bounded_distrib_lattice α] :
bounded_lattice α
source
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
source
@[protected, instance]
def bounded_distrib_lattice_Prop  :
bounded_distrib_lattice Prop

Propositions form a bounded distributive lattice.

Equations
source
@[protected, instance]
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)
source
@[protected, instance]
def pi.order_bot {α : Type u_1} {β : α → Type u_2} [Π (a : α), order_bot (β a)] :
order_bot (Π (a : α), β a)
Equations
source
@[protected, instance]
def pi.has_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_sup (α i)] :
has_sup (Π (i : ι), α i)
Equations
source
@[simp]
theorem sup_apply {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_sup (α i)] (f g : Π (i : ι), α i) (i : ι) :
(f ⊔ g) i = f i ⊔ g i
source
@[protected, instance]
def pi.has_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_inf (α i)] :
has_inf (Π (i : ι), α i)
Equations
source
@[simp]
theorem inf_apply {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_inf (α i)] (f g : Π (i : ι), α i) (i : ι) :
(f ⊓ g) i = f i ⊓ g i
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 bot_apply {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_bot (α i)] (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 top_apply {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_top (α i)] (i : ι) :
⊤ i = ⊤
source
@[protected, instance]
def pi.semilattice_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup (α i)] :
semilattice_sup (Π (i : ι), α i)
Equations
source
@[protected, instance]
def pi.semilattice_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf (α i)] :
semilattice_inf (Π (i : ι), α i)
Equations
source
@[protected, instance]
def pi.semilattice_inf_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_bot (α i)] :
semilattice_inf_bot (Π (i : ι), α i)
Equations
source
@[protected, instance]
def pi.semilattice_inf_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_top (α i)] :
semilattice_inf_top (Π (i : ι), α i)
Equations
source
@[protected, instance]
def pi.semilattice_sup_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_bot (α i)] :
semilattice_sup_bot (Π (i : ι), α i)
Equations
source
@[protected, instance]
def pi.semilattice_sup_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_top (α i)] :
semilattice_sup_top (Π (i : ι), α i)
Equations
source
@[protected, instance]
def pi.lattice {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), lattice (α i)] :
lattice (Π (i : ι), α i)
Equations
source
@[protected, instance]
def pi.bounded_lattice {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] :
bounded_lattice (Π (i : ι), α i)
Equations
source
theorem eq_bot_of_bot_eq_top {α : Type u_1} [bounded_lattice α] (hα : ⊥ = ⊤) (x : α) :
x = ⊥
source
theorem eq_top_of_bot_eq_top {α : Type u_1} [bounded_lattice α] (hα : ⊥ = ⊤) (x : α) :
x = ⊤
source
theorem subsingleton_of_top_le_bot {α : Type u_1} [bounded_lattice α] (h : ⊤ ≤ ⊥) :
subsingleton α
source
theorem subsingleton_of_bot_eq_top {α : Type u_1} [bounded_lattice α] (hα : ⊥ = ⊤) :
subsingleton α
source
theorem subsingleton_iff_bot_eq_top {α : Type u_1} [bounded_lattice α] :
⊥ = ⊤ ↔ subsingleton α
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
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
@[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.bot_lt_some {α : Type u} [has_lt α] (a : α) :
⊥ < some a
source
theorem with_bot.bot_lt_coe {α : Type u} [has_lt α] (a : α) :
⊥ < ↑a
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} [partial_order α] :
order_bot (with_bot α)
Equations
source
@[simp, norm_cast]
theorem with_bot.coe_le_coe {α : Type u} [preorder α] {a b : α} :
↑a ≤ ↑b ↔ a ≤ b
source
@[simp]
theorem with_bot.some_le_some {α : Type u} [preorder α] {a b : α} :
some a ≤ some b ↔ a ≤ b
source
theorem with_bot.coe_le {α : Type u} [partial_order α] {a b : α} {o : option α} :
b ∈ o → (↑a ≤ o ↔ a ≤ b)
source
@[norm_cast]
theorem with_bot.coe_lt_coe {α : Type u} [partial_order α] {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} [order_bot α] {a : with_bot α} {b : α} :
option.get_or_else a ⊥ ≤ b ↔ a ≤ ↑b
source
@[protected, instance]
def with_bot.decidable_le {α : Type u} [preorder α] [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.linear_order {α : Type u} [linear_order α] :
linear_order (with_bot α)
Equations
source
@[protected, instance]
def with_bot.semilattice_sup {α : Type u} [semilattice_sup α] :
semilattice_sup_bot (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_bot (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
theorem with_bot.lattice_eq_DLO {α : Type u} [linear_order α] :
lattice_of_linear_order = with_bot.lattice
source
theorem with_bot.sup_eq_max {α : Type u} [linear_order α] (x y : with_bot α) :
x ⊔ y = max x y
source
theorem with_bot.inf_eq_min {α : Type u} [linear_order α] (x y : with_bot α) :
x ⊓ y = min x y
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} [order_top α] :
order_top (with_bot α)
Equations
source
@[protected, instance]
def with_bot.bounded_lattice {α : Type u} [bounded_lattice α] :
bounded_lattice (with_bot α)
Equations
source
theorem with_bot.well_founded_lt {α : Type u} [partial_order α] (h : well_founded has_lt.lt) :
well_founded has_lt.lt
source
@[protected, instance]
def with_bot.densely_ordered {α : Type u} [partial_order α] [densely_ordered α] [no_bot_order α] :
densely_ordered (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
@[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
@[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} [partial_order α] :
order_top (with_top α)
Equations
source
@[simp, norm_cast]
theorem with_top.coe_le_coe {α : Type u} [partial_order α] {a b : α} :
↑a ≤ ↑b ↔ a ≤ b
source
theorem with_top.le_coe {α : Type u} [partial_order α] {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} [partial_order α] {a b : α} :
↑a < ↑b ↔ a < b
source
theorem with_top.coe_lt_top {α : Type u} [partial_order α] (a : α) :
↑a < ⊤
source
theorem with_top.coe_lt_iff {α : Type u} [partial_order α] {a : α} {x : with_top α} :
↑a < x ↔ ∀ (b : α), x = ↑b → a < b
source
theorem with_top.not_top_le_coe {α : Type u} [partial_order α] (a : α) :
¬⊤ ≤ ↑a
source
@[protected, instance]
def with_top.decidable_le {α : Type u} [preorder α] [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.linear_order {α : Type u} [linear_order α] :
linear_order (with_top α)
Equations
source
@[protected, instance]
def with_top.semilattice_inf {α : Type u} [semilattice_inf α] :
semilattice_inf_top (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_top (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
theorem with_top.lattice_eq_DLO {α : Type u} [linear_order α] :
lattice_of_linear_order = with_top.lattice
source
theorem with_top.sup_eq_max {α : Type u} [linear_order α] (x y : with_top α) :
x ⊔ y = max x y
source
theorem with_top.inf_eq_min {α : Type u} [linear_order α] (x y : with_top α) :
x ⊓ y = min x y
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} [order_bot α] :
order_bot (with_top α)
Equations
source
@[protected, instance]
def with_top.bounded_lattice {α : Type u} [bounded_lattice α] :
bounded_lattice (with_top α)
Equations
source
theorem with_top.well_founded_lt {α : Type u_1} [partial_order α] (h : well_founded has_lt.lt) :
well_founded has_lt.lt
source
@[protected, instance]
def with_top.densely_ordered {α : Type u} [partial_order α] [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]
def subtype.semilattice_sup_bot {α : Type u} [semilattice_sup_bot α] {P : α → Prop} (Pbot : P ⊥) (Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) :
semilattice_sup_bot {x // P x}

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

Equations
source
@[protected]
def subtype.semilattice_inf_bot {α : Type u} [semilattice_inf_bot α] {P : α → Prop} (Pbot : P ⊥) (Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) :
semilattice_inf_bot {x // P x}

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

Equations
source
@[protected]
def subtype.semilattice_inf_top {α : Type u} [semilattice_inf_top α] {P : α → Prop} (Ptop : P ⊤) (Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) :
semilattice_inf_top {x // P x}

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

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) [order_bot α] :
order_top (order_dual α)
Equations
source
@[protected, instance]
def order_dual.order_bot (α : Type u) [order_top α] :
order_bot (order_dual α)
Equations
source
@[protected, instance]
def order_dual.semilattice_sup_top (α : Type u) [semilattice_inf_bot α] :
semilattice_sup_top (order_dual α)
Equations
source
@[protected, instance]
def order_dual.semilattice_sup_bot (α : Type u) [semilattice_inf_top α] :
semilattice_sup_bot (order_dual α)
Equations
source
@[protected, instance]
def order_dual.semilattice_inf_top (α : Type u) [semilattice_sup_bot α] :
semilattice_inf_top (order_dual α)
Equations
source
@[protected, instance]
def order_dual.semilattice_inf_bot (α : Type u) [semilattice_sup_top α] :
semilattice_inf_bot (order_dual α)
Equations
source
@[protected, instance]
def order_dual.bounded_lattice (α : Type u) [bounded_lattice α] :
bounded_lattice (order_dual α)
Equations
source
@[protected, instance]
def order_dual.bounded_distrib_lattice (α : Type u) [bounded_distrib_lattice α] :
bounded_distrib_lattice (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) [order_top α] [order_top β] :
order_top (α × β)
Equations
source
@[protected, instance]
def prod.order_bot (α : Type u) (β : Type v) [order_bot α] [order_bot β] :
order_bot (α × β)
Equations
source
@[protected, instance]
def prod.semilattice_sup_top (α : Type u) (β : Type v) [semilattice_sup_top α] [semilattice_sup_top β] :
semilattice_sup_top (α × β)
Equations
source
@[protected, instance]
def prod.semilattice_inf_top (α : Type u) (β : Type v) [semilattice_inf_top α] [semilattice_inf_top β] :
semilattice_inf_top (α × β)
Equations
source
@[protected, instance]
def prod.semilattice_sup_bot (α : Type u) (β : Type v) [semilattice_sup_bot α] [semilattice_sup_bot β] :
semilattice_sup_bot (α × β)
Equations
source
@[protected, instance]
def prod.semilattice_inf_bot (α : Type u) (β : Type v) [semilattice_inf_bot α] [semilattice_inf_bot β] :
semilattice_inf_bot (α × β)
Equations
source
@[protected, instance]
def prod.bounded_lattice (α : Type u) (β : Type v) [bounded_lattice α] [bounded_lattice β] :
bounded_lattice (α × β)
Equations
source
@[protected, instance]
def prod.bounded_distrib_lattice (α : Type u) (β : Type v) [bounded_distrib_lattice α] [bounded_distrib_lattice β] :
bounded_distrib_lattice (α × β)
Equations
source
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
source
theorem disjoint.eq_bot {α : Type u} [semilattice_inf_bot α] {a b : α} (h : disjoint a b) :
a ⊓ b = ⊥
source
theorem disjoint_iff {α : Type u} [semilattice_inf_bot α] {a b : α} :
disjoint a b ↔ a ⊓ b = ⊥
source
theorem disjoint.comm {α : Type u} [semilattice_inf_bot α] {a b : α} :
disjoint a b ↔ disjoint b a
source
theorem disjoint.symm {α : Type u} [semilattice_inf_bot α] ⦃a b : α⦄ :
disjoint a b → disjoint b a
source
@[simp]
theorem disjoint_bot_left {α : Type u} [semilattice_inf_bot α] {a : α} :
disjoint ⊥ a
source
@[simp]
theorem disjoint_bot_right {α : Type u} [semilattice_inf_bot α] {a : α} :
disjoint a ⊥
source
theorem disjoint.mono {α : Type u} [semilattice_inf_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_bot α] {a b c : α} (h : a ≤ b) :
disjoint b c → disjoint a c
source
theorem disjoint.mono_right {α : Type u} [semilattice_inf_bot α] {a b c : α} (h : b ≤ c) :
disjoint a c → disjoint a b
source
@[simp]
theorem disjoint_self {α : Type u} [semilattice_inf_bot α] {a : α} :
disjoint a a ↔ a = ⊥
source
theorem disjoint.ne {α : Type u} [semilattice_inf_bot α] {a b : α} (ha : a ≠ ⊥) (hab : disjoint a b) :
a ≠ b
source
@[simp]
theorem disjoint_top {α : Type u} [bounded_lattice α] {a : α} :
disjoint a ⊤ ↔ a = ⊥
source
@[simp]
theorem top_disjoint {α : Type u} [bounded_lattice α] {a : α} :
disjoint ⊤ a ↔ a = ⊥
source
@[simp]
theorem disjoint_sup_left {α : Type u} [bounded_distrib_lattice α] {a b c : α} :
disjoint (a ⊔ b) c ↔ disjoint a c ∧ disjoint b c
source
@[simp]
theorem disjoint_sup_right {α : Type u} [bounded_distrib_lattice α] {a b c : α} :
disjoint a (b ⊔ c) ↔ disjoint a b ∧ disjoint a c
source
theorem disjoint.sup_left {α : Type u} [bounded_distrib_lattice α] {a b c : α} (ha : disjoint a c) (hb : disjoint b c) :
disjoint (a ⊔ b) c
source
theorem disjoint.sup_right {α : Type u} [bounded_distrib_lattice α] {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} [bounded_distrib_lattice α] {a b c : α} (h : a ≤ b ⊔ c) (hd : disjoint a c) :
a ≤ b
source
theorem disjoint.left_le_of_le_sup_left {α : Type u} [bounded_distrib_lattice α] {a b c : α} (h : a ≤ c ⊔ b) (hd : disjoint a c) :
a ≤ b

is_compl predicate #

source
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 = ⊥.

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