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 maximal 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) [s : order_top α] :
partial_order α

source
@[instance]
def order_top.to_has_top (α : Type u) [s : 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 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 minimal 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) [s : order_bot α] :
partial_order α

source
@[instance]
def order_bot.to_has_bot (α : Type u) [s : 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 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) [s : semilattice_sup_top α] :
order_top α

source
@[instance]
def semilattice_sup_top.to_semilattice_sup (α : Type u) [s : 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) [s : semilattice_sup_bot α] :
order_bot α

source
@[instance]
def semilattice_sup_bot.to_semilattice_sup (α : Type u) [s : 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
@[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) [s : semilattice_inf_top α] :
order_top α

source
@[instance]
def semilattice_inf_top.to_semilattice_inf (α : Type u) [s : 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) [s : 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) [s : 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) [s : bounded_lattice α] :
order_top α

source
@[instance]
def bounded_lattice.to_order_bot (α : Type u) [s : bounded_lattice α] :
order_bot α

source
@[instance]
def bounded_lattice.to_lattice (α : Type u) [s : 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
@[instance]
def semilattice_inf_top_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :
semilattice_inf_top α

Equations
source
@[instance]
def semilattice_inf_bot_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :
semilattice_inf_bot α

Equations
source
@[instance]
def semilattice_sup_top_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :
semilattice_sup_top α

Equations
source
@[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) [s : 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) [s : 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
@[instance]
def bounded_distrib_lattice_Prop  :
bounded_distrib_lattice Prop

Equations
source
@[instance]
def Prop.linear_order  :
linear_order Prop

Equations
source
@[simp]
theorem le_iff_imp {p q : Prop} :
p ≤ q ↔ p → q

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
@[instance]
def pi.order_bot {α : Type u_1} {β : α → Type u_2} [Π (a : α), order_bot (β a)] :
order_bot (Π (a : α), β a)

Equations
source
@[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
@[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
@[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
@[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
@[simp]
theorem pi.semilattice_sup_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
semilattice_sup.sup a a_1 i = (a ⊔ a_1) i

source
@[instance]
def pi.semilattice_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup (α i)] :
semilattice_sup (Π (i : ι), α i)

Equations
source
@[simp]
theorem pi.semilattice_sup_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup (α i)] (a a_1 : Π (i : ι), α i) :
a ≤ a_1 = partial_order.le a a_1

source
@[simp]
theorem pi.semilattice_sup_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = partial_order.lt a a_1

source
@[simp]
theorem pi.semilattice_inf_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
semilattice_inf.inf a a_1 i = (a ⊓ a_1) i

source
@[instance]
def pi.semilattice_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf (α i)] :
semilattice_inf (Π (i : ι), α i)

Equations
source
@[simp]
theorem pi.semilattice_inf_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = partial_order.lt a a_1

source
@[simp]
theorem pi.semilattice_inf_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf (α i)] (a a_1 : Π (i : ι), α i) :
a ≤ a_1 = partial_order.le a a_1

source
@[simp]
theorem pi.semilattice_inf_bot_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_bot (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
semilattice_inf_bot.inf a a_1 i = (a ⊓ a_1) i

source
@[simp]
theorem pi.semilattice_inf_bot_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_bot (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = partial_order.lt a a_1

source
@[instance]
def pi.semilattice_inf_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_bot (α i)] :
semilattice_inf_bot (Π (i : ι), α i)

Equations
source
@[simp]
theorem pi.semilattice_inf_bot_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_bot (α i)] (i : ι) :
semilattice_inf_bot.bot i = ⊥ i

source
@[simp]
theorem pi.semilattice_inf_bot_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_bot (α i)] (a a_1 : Π (i : ι), α i) :
a ≤ a_1 = partial_order.le a a_1

source
@[simp]
theorem pi.semilattice_inf_top_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_top (α i)] (a a_1 : Π (i : ι), α i) :
a ≤ a_1 = partial_order.le a a_1

source
@[instance]
def pi.semilattice_inf_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_top (α i)] :
semilattice_inf_top (Π (i : ι), α i)

Equations
source
@[simp]
theorem pi.semilattice_inf_top_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_top (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = partial_order.lt a a_1

source
@[simp]
theorem pi.semilattice_inf_top_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_top (α i)] (i : ι) :
semilattice_inf_top.top i = ⊤ i

source
@[simp]
theorem pi.semilattice_inf_top_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_inf_top (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
semilattice_inf_top.inf a a_1 i = (a ⊓ a_1) i

source
@[simp]
theorem pi.semilattice_sup_bot_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_bot (α i)] (a a_1 : Π (i : ι), α i) :
a ≤ a_1 = partial_order.le a a_1

source
@[simp]
theorem pi.semilattice_sup_bot_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_bot (α i)] (i : ι) :
semilattice_sup_bot.bot i = ⊥ i

source
@[simp]
theorem pi.semilattice_sup_bot_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_bot (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
semilattice_sup_bot.sup a a_1 i = (a ⊔ a_1) i

source
@[simp]
theorem pi.semilattice_sup_bot_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_bot (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = partial_order.lt a a_1

source
@[instance]
def pi.semilattice_sup_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_bot (α i)] :
semilattice_sup_bot (Π (i : ι), α i)

Equations
source
@[simp]
theorem pi.semilattice_sup_top_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_top (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
semilattice_sup_top.sup a a_1 i = (a ⊔ a_1) i

source
@[simp]
theorem pi.semilattice_sup_top_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_top (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = partial_order.lt a a_1

source
@[instance]
def pi.semilattice_sup_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_top (α i)] :
semilattice_sup_top (Π (i : ι), α i)

Equations
source
@[simp]
theorem pi.semilattice_sup_top_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_top (α i)] (a a_1 : Π (i : ι), α i) :
a ≤ a_1 = partial_order.le a a_1

source
@[simp]
theorem pi.semilattice_sup_top_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), semilattice_sup_top (α i)] (i : ι) :
semilattice_sup_top.top i = ⊤ i

source
@[simp]
theorem pi.lattice_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), lattice (α i)] (a a_1 : Π (i : ι), α i) :
a ≤ a_1 = semilattice_sup.le a a_1

source
@[instance]
def pi.lattice {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), lattice (α i)] :
lattice (Π (i : ι), α i)

Equations
source
@[simp]
theorem pi.lattice_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), lattice (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
lattice.inf a a_1 i = semilattice_inf.inf a a_1 i

source
@[simp]
theorem pi.lattice_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), lattice (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = semilattice_sup.lt a a_1

source
@[simp]
theorem pi.lattice_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), lattice (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
lattice.sup a a_1 i = semilattice_sup.sup a a_1 i

source
@[instance]
def pi.bounded_lattice {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] :
bounded_lattice (Π (i : ι), α i)

Equations
source
@[simp]
theorem pi.bounded_lattice_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
bounded_lattice.sup a a_1 i = semilattice_sup_top.sup a a_1 i

source
@[simp]
theorem pi.bounded_lattice_top {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] (i : ι) :
bounded_lattice.top i = semilattice_sup_top.top i

source
@[simp]
theorem pi.bounded_lattice_inf {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] (a a_1 : Π (i : ι), α i) (i : ι) :
bounded_lattice.inf a a_1 i = semilattice_inf_bot.inf a a_1 i

source
@[simp]
theorem pi.bounded_lattice_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] (i : ι) :
bounded_lattice.bot i = semilattice_inf_bot.bot i

source
@[simp]
theorem pi.bounded_lattice_le {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] (a a_1 : Π (i : ι), α i) :
a ≤ a_1 = semilattice_sup_top.le a a_1

source
@[simp]
theorem pi.bounded_lattice_lt {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), bounded_lattice (α i)] (a a_1 : Π (i : ι), α i) :
a < a_1 = semilattice_sup_top.lt a a_1

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

Attach ⊥ to a type.

Equations
source
@[instance]
meta def with_bot.has_to_format {α : Type u_1} [has_to_format α] :
has_to_format (with_bot α)

source
@[instance]
def with_bot.has_coe_t {α : Type u} :
has_coe_t α (with_bot α)

Equations
source
@[instance]
def with_bot.has_bot {α : Type u} :
has_bot (with_bot α)

Equations
source
@[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
theorem with_bot.coe_eq_coe {α : Type u} {a b : α} :
↑a = ↑b ↔ a = b

source
@[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
@[instance]
def with_bot.preorder {α : Type u} [preorder α] :
preorder (with_bot α)

Equations
source
@[instance]
def with_bot.partial_order {α : Type u} [partial_order α] :
partial_order (with_bot α)

Equations
source
@[instance]
def with_bot.order_bot {α : Type u} [partial_order α] :
order_bot (with_bot α)

Equations
source
@[simp]
theorem with_bot.coe_le_coe {α : Type u} [partial_order α] {a b : α} :
↑a ≤ ↑b ↔ a ≤ b

source
@[simp]
theorem with_bot.some_le_some {α : Type u} [partial_order α] {a b : α} :
some a ≤ some b ↔ a ≤ b

source
theorem with_bot.coe_le {α : Type u} [partial_order α] {a b : α} {o : option α} (a_1 : b ∈ o) :
↑a ≤ o ↔ a ≤ b

source
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
@[instance]
def with_bot.linear_order {α : Type u} [linear_order α] :
linear_order (with_bot α)

Equations
source
@[instance]
def with_bot.decidable_lt {α : Type u} [has_lt α] [decidable_rel has_lt.lt] :
decidable_rel has_lt.lt

Equations
source
@[instance]
def with_bot.decidable_linear_order {α : Type u} [decidable_linear_order α] :
decidable_linear_order (with_bot α)

Equations
source
@[instance]
def with_bot.semilattice_sup {α : Type u} [semilattice_sup α] :
semilattice_sup_bot (with_bot α)

Equations
source
@[instance]
def with_bot.semilattice_inf {α : Type u} [semilattice_inf α] :
semilattice_inf_bot (with_bot α)

Equations
source
@[instance]
def with_bot.lattice {α : Type u} [lattice α] :
lattice (with_bot α)

Equations
source
theorem with_bot.lattice_eq_DLO {α : Type u} [decidable_linear_order α] :
lattice_of_decidable_linear_order = with_bot.lattice

source
theorem with_bot.sup_eq_max {α : Type u} [decidable_linear_order α] (x y : with_bot α) :
x ⊔ y = max x y

source
theorem with_bot.inf_eq_min {α : Type u} [decidable_linear_order α] (x y : with_bot α) :
x ⊓ y = min x y

source
@[instance]
def with_bot.order_top {α : Type u} [order_top α] :
order_top (with_bot α)

Equations
source
@[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
@[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

Equations
source
@[instance]
meta def with_top.has_to_format {α : Type u_1} [has_to_format α] :
has_to_format (with_top α)

source
@[instance]
def with_top.has_coe_t {α : Type u} :
has_coe_t α (with_top α)

Equations
source
@[instance]
def with_top.has_top {α : Type u} :
has_top (with_top α)

Equations
source
@[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
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
@[instance]
def with_top.has_lt {α : Type u} [has_lt α] :
has_lt (with_top α)

Equations
source
@[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
@[instance]
def with_top.preorder {α : Type u} [preorder α] :
preorder (with_top α)

Equations
source
@[instance]
def with_top.partial_order {α : Type u} [partial_order α] :
partial_order (with_top α)

Equations
source
@[instance]
def with_top.order_top {α : Type u} [partial_order α] :
order_top (with_top α)

Equations
source
@[simp]
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_1 : 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
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.not_top_le_coe {α : Type u} [partial_order α] (a : α) :
¬⊤ ≤ ↑a

source
@[instance]
def with_top.linear_order {α : Type u} [linear_order α] :
linear_order (with_top α)

Equations
source
@[instance]
def with_top.decidable_linear_order {α : Type u} [decidable_linear_order α] :
decidable_linear_order (with_top α)

Equations
source
@[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
@[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
@[instance]
def with_top.lattice {α : Type u} [lattice α] :
lattice (with_top α)

Equations
source
theorem with_top.lattice_eq_DLO {α : Type u} [decidable_linear_order α] :
lattice_of_decidable_linear_order = with_top.lattice

source
theorem with_top.sup_eq_max {α : Type u} [decidable_linear_order α] (x y : with_top α) :
x ⊔ y = max x y

source
theorem with_top.inf_eq_min {α : Type u} [decidable_linear_order α] (x y : with_top α) :
x ⊓ y = min x y

source
@[instance]
def with_top.order_bot {α : Type u} [order_bot α] :
order_bot (with_top α)

Equations
source
@[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
@[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
def subtype.semilattice_sup {α : Type u} [semilattice_sup α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) :
semilattice_sup {x // P x}

A subtype forms a ⊔-semilattice if ⊔ preserves the property.

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

A subtype forms a ⊓-semilattice if ⊓ preserves the property.

Equations
source
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
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
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
def subtype.lattice {α : Type u} [lattice α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) :
lattice {x // P x}

A subtype forms a lattice if ⊔ and ⊓ preserve the property.

Equations
source
@[instance]
def order_dual.has_top (α : Type u) [has_bot α] :
has_top (order_dual α)

Equations
source
@[instance]
def order_dual.has_bot (α : Type u) [has_top α] :
has_bot (order_dual α)

Equations
source
@[instance]
def order_dual.order_top (α : Type u) [order_bot α] :
order_top (order_dual α)

Equations
source
@[instance]
def order_dual.order_bot (α : Type u) [order_top α] :
order_bot (order_dual α)

Equations
source
@[instance]
def order_dual.semilattice_sup_top (α : Type u) [semilattice_inf_bot α] :
semilattice_sup_top (order_dual α)

Equations
source
@[instance]
def order_dual.semilattice_sup_bot (α : Type u) [semilattice_inf_top α] :
semilattice_sup_bot (order_dual α)

Equations
source
@[instance]
def order_dual.semilattice_inf_top (α : Type u) [semilattice_sup_bot α] :
semilattice_inf_top (order_dual α)

Equations
source
@[instance]
def order_dual.semilattice_inf_bot (α : Type u) [semilattice_sup_top α] :
semilattice_inf_bot (order_dual α)

Equations
source
@[instance]
def order_dual.bounded_lattice (α : Type u) [bounded_lattice α] :
bounded_lattice (order_dual α)

Equations
source
@[instance]
def order_dual.bounded_distrib_lattice (α : Type u) [bounded_distrib_lattice α] :
bounded_distrib_lattice (order_dual α)

Equations
source
@[instance]
def prod.has_top (α : Type u) (β : Type v) [has_top α] [has_top β] :
has_top (α × β)

Equations
source
@[instance]
def prod.has_bot (α : Type u) (β : Type v) [has_bot α] [has_bot β] :
has_bot (α × β)

Equations
source
@[instance]
def prod.order_top (α : Type u) (β : Type v) [order_top α] [order_top β] :
order_top (α × β)

Equations
source
@[instance]
def prod.order_bot (α : Type u) (β : Type v) [order_bot α] [order_bot β] :
order_bot (α × β)

Equations
source
@[instance]
def prod.semilattice_sup_top (α : Type u) (β : Type v) [semilattice_sup_top α] [semilattice_sup_top β] :
semilattice_sup_top (α × β)

Equations
source
@[instance]
def prod.semilattice_inf_top (α : Type u) (β : Type v) [semilattice_inf_top α] [semilattice_inf_top β] :
semilattice_inf_top (α × β)

Equations
source
@[instance]
def prod.semilattice_sup_bot (α : Type u) (β : Type v) [semilattice_sup_bot α] [semilattice_sup_bot β] :
semilattice_sup_bot (α × β)

Equations
source
@[instance]
def prod.semilattice_inf_bot (α : Type u) (β : Type v) [semilattice_inf_bot α] [semilattice_inf_bot β] :
semilattice_inf_bot (α × β)

Equations
source
@[instance]
def prod.bounded_lattice (α : Type u) (β : Type v) [bounded_lattice α] [bounded_lattice β] :
bounded_lattice (α × β)

Equations
source
@[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 : α⦄ (a_1 : 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) (a_1 : disjoint b d) :
disjoint a c

source
theorem disjoint.mono_left {α : Type u} [semilattice_inf_bot α] {a b c : α} (h : a ≤ b) (a_1 : disjoint b c) :
disjoint a c

source
theorem disjoint.mono_right {α : Type u} [semilattice_inf_bot α] {a b c : α} (h : b ≤ c) (a_1 : 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_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)

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
theorem is_compl.disjoint {α : Type u} [bounded_lattice α] {x y : α} (h : is_compl x y) :
disjoint x y

source
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.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.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_bot_top {α : Type u} [bounded_lattice α] :
is_compl ⊥ ⊤

source
theorem is_compl_top_bot {α : Type u} [bounded_lattice α] :
is_compl ⊤ ⊥