mathlib docs: order.bounded

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

@[instance]

def order_top.to_has_top (α : Type u) [s : order_top α] :

has_top α

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

@[simp]

theorem le_top {α : Type u} [order_top α] {a : α} :

a ≤ ⊤

source

theorem top_unique {α : Type u} [order_top α] {a : α} :

⊤ ≤ 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 : α} :

a ≤ b → 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 : α} :

a < b → a ≠ ⊤

source

theorem ne_top_of_le_ne_top {α : Type u} [order_top α] {a b : α} :

b ≠ ⊤ → a ≤ b → a ≠ ⊤

source

theorem order_top.ext_top {α : Type u_1} {A B : order_top α} :

(∀ (x y : α), x ≤ y ↔ x ≤ y) → ⊤ = ⊤

source

theorem order_top.ext {α : Type u_1} {A B : order_top α} :

(∀ (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_has_bot (α : Type u) [s : order_bot α] :

has_bot α

source

@[instance]

def order_bot.to_partial_order (α : Type u) [s : order_bot α] :

partial_order α

source

@[simp]

theorem bot_le {α : Type u} [order_bot α] {a : α} :

⊥ ≤ a

source

theorem bot_unique {α : Type u} [order_bot α] {a : α} :

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 : α} :

b ≠ ⊥ → b ≤ a → a ≠ ⊥

source

theorem eq_bot_mono {α : Type u} [order_bot α] {a b : α} :

a ≤ b → 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 : α} :

a < b → b ≠ ⊥

source

theorem order_bot.ext_bot {α : Type u_1} {A B : order_bot α} :

(∀ (x y : α), x ≤ y ↔ x ≤ y) → ⊥ = ⊥

source

theorem order_bot.ext {α : Type u_1} {A B : order_bot α} :

(∀ (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_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

@[instance]

def semilattice_sup_bot.to_order_bot (α : Type u) [s : semilattice_sup_bot α] :

order_bot α

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

nat.semilattice_sup_bot = {bot := 0, le := distrib_lattice.le nat.distrib_lattice, lt := distrib_lattice.lt nat.distrib_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := nat.zero_le, sup := distrib_lattice.sup nat.distrib_lattice, le_sup_left := _, le_sup_right := _, sup_le := _}

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

@[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_order_bot (α : Type u) [s : semilattice_inf_bot α] :

order_bot α

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_lattice (α : Type u) [s : bounded_lattice α] :

lattice α

source

@[instance]

def bounded_lattice.to_order_bot (α : Type u) [s : bounded_lattice α] :

order_bot α

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 bounded_lattice.to_order_top (α : Type u) [s : bounded_lattice α] :

order_top α

source

@[instance]

def semilattice_inf_top_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :

semilattice_inf_top α

Equations

semilattice_inf_top_of_bounded_lattice α = {top := bounded_lattice.top bl, le := bounded_lattice.le bl, lt := bounded_lattice.lt bl, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, inf := bounded_lattice.inf bl, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def semilattice_inf_bot_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :

semilattice_inf_bot α

Equations

semilattice_inf_bot_of_bounded_lattice α = {bot := bounded_lattice.bot bl, le := bounded_lattice.le bl, lt := bounded_lattice.lt bl, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := bounded_lattice.inf bl, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def semilattice_sup_top_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :

semilattice_sup_top α

Equations

semilattice_sup_top_of_bounded_lattice α = {top := bounded_lattice.top bl, le := bounded_lattice.le bl, lt := bounded_lattice.lt bl, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := bounded_lattice.sup bl, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def semilattice_sup_bot_of_bounded_lattice (α : Type u) [bl : bounded_lattice α] :

semilattice_sup_bot α

Equations

semilattice_sup_bot_of_bounded_lattice α = {bot := bounded_lattice.bot bl, le := bounded_lattice.le bl, lt := bounded_lattice.lt bl, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := bounded_lattice.sup bl, le_sup_left := _, le_sup_right := _, sup_le := _}

source

theorem bounded_lattice.ext {α : Type u_1} {A B : bounded_lattice α} :

(∀ (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 : α} :

b ⊔ c = ⊤ → b ⊓ c = ⊥ → (a ⊓ b = ⊥ ↔ a ≤ c)

source

@[instance]

def bounded_distrib_lattice_Prop :

bounded_distrib_lattice Prop

Equations

bounded_distrib_lattice_Prop = {sup := or, le := λ (a b : Prop), a → b, lt := distrib_lattice.lt._default (λ (a b : Prop), a → b), le_refl := bounded_distrib_lattice_Prop._proof_1, le_trans := bounded_distrib_lattice_Prop._proof_2, lt_iff_le_not_le := bounded_distrib_lattice_Prop._proof_3, le_antisymm := bounded_distrib_lattice_Prop._proof_4, le_sup_left := or.inl, le_sup_right := or.inr, sup_le := bounded_distrib_lattice_Prop._proof_5, inf := and, inf_le_left := and.left, inf_le_right := and.right, le_inf := bounded_distrib_lattice_Prop._proof_6, le_sup_inf := bounded_distrib_lattice_Prop._proof_7, top := true, le_top := bounded_distrib_lattice_Prop._proof_8, bot := false, bot_le := false.elim}

source

theorem monotone_and {α : Type u} [preorder α] {p q : α → Prop} :

monotone p → monotone q → monotone (λ (x : α), p x ∧ q x)

source

theorem monotone_or {α : Type u} [preorder α] {p q : α → Prop} :

monotone p → monotone q → monotone (λ (x : α), p x ∨ q x)

source

@[instance]

def pi.has_sup {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_sup (α i)] :

has_sup (Π (i : ι), α i)

Equations

pi.has_sup = {sup := λ (f g : Π (i : ι), α i) (i : ι), f i ⊔ g i}

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

pi.has_inf = {inf := λ (f g : Π (i : ι), α i) (i : ι), f i ⊓ g i}

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

pi.has_bot = {bot := λ (i : ι), ⊥}

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

pi.has_top = {top := λ (i : ι), ⊤}

source

@[simp]

theorem top_apply {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), has_top (α i)] (i : ι) :

⊤ i = ⊤

source

@[instance]

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

semilattice_sup (Π (i : ι), α i)

Equations

pi.semilattice_sup = {sup := has_sup.sup pi.has_sup, le := partial_order.le pi.partial_order, lt := partial_order.lt pi.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

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

semilattice_inf (Π (i : ι), α i)

Equations

pi.semilattice_inf = {inf := has_inf.inf pi.has_inf, le := partial_order.le pi.partial_order, lt := partial_order.lt pi.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

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

semilattice_inf_bot (Π (i : ι), α i)

Equations

pi.semilattice_inf_bot = {bot := ⊥, le := partial_order.le pi.partial_order, lt := partial_order.lt pi.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := has_inf.inf pi.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

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

semilattice_inf_top (Π (i : ι), α i)

Equations

pi.semilattice_inf_top = {top := ⊤, le := partial_order.le pi.partial_order, lt := partial_order.lt pi.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, inf := has_inf.inf pi.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

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

semilattice_sup_bot (Π (i : ι), α i)

Equations

pi.semilattice_sup_bot = {bot := ⊥, le := partial_order.le pi.partial_order, lt := partial_order.lt pi.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := has_sup.sup pi.has_sup, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

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

semilattice_sup_top (Π (i : ι), α i)

Equations

pi.semilattice_sup_top = {top := ⊤, le := partial_order.le pi.partial_order, lt := partial_order.lt pi.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := has_sup.sup pi.has_sup, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

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

lattice (Π (i : ι), α i)

Equations

pi.lattice = {sup := semilattice_sup.sup pi.semilattice_sup, le := semilattice_sup.le pi.semilattice_sup, lt := semilattice_sup.lt pi.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf pi.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

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

bounded_lattice (Π (i : ι), α i)

Equations

pi.bounded_lattice = {sup := semilattice_sup_top.sup pi.semilattice_sup_top, le := semilattice_sup_top.le pi.semilattice_sup_top, lt := semilattice_sup_top.lt pi.semilattice_sup_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf_bot.inf pi.semilattice_inf_bot, inf_le_left := _, inf_le_right := _, le_inf := _, top := semilattice_sup_top.top pi.semilattice_sup_top, le_top := _, bot := semilattice_inf_bot.bot pi.semilattice_inf_bot, bot_le := _}

source

def with_bot :

Type u_1 → Type u_1

Attach ⊥ to a type.

Equations

with_bot α = option α

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

with_bot.has_coe_t = {coe := option.some α}

source

@[instance]

def with_bot.has_bot {α : Type u} :

has_bot (with_bot α)

Equations

with_bot.has_bot = {bot := option.none α}

source

@[instance]

def with_bot.inhabited {α : Type u} :

inhabited (with_bot α)

Equations

with_bot.inhabited = {default := ⊥}

source

theorem with_bot.none_eq_bot {α : Type u} :

option.none = ⊥

source

theorem with_bot.some_eq_coe {α : Type u} (a : α) :

option.some a = ↑a

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

with_bot.has_lt = {lt := λ (o₁ o₂ : option α), ∃ (b : α) (H : b ∈ o₂), ∀ (a : α), a ∈ o₁ → a < b}

source

@[simp]

theorem with_bot.some_lt_some {α : Type u} [has_lt α] {a b : α} :

option.some a < option.some b ↔ a < b

source

theorem with_bot.bot_lt_some {α : Type u} [has_lt α] (a : α) :

⊥ < option.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

with_bot.preorder = {le := λ (o₁ o₂ : option α), ∀ (a : α), a ∈ o₁ → (∃ (b : α) (H : b ∈ o₂), a ≤ b), lt := has_lt.lt with_bot.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

source

@[instance]

def with_bot.partial_order {α : Type u} [partial_order α] :

partial_order (with_bot α)

Equations

with_bot.partial_order = {le := preorder.le with_bot.preorder, lt := preorder.lt with_bot.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[instance]

def with_bot.order_bot {α : Type u} [partial_order α] :

order_bot (with_bot α)

Equations

with_bot.order_bot = {bot := ⊥, le := partial_order.le with_bot.partial_order, lt := partial_order.lt with_bot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}

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 : α} :

option.some a ≤ option.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

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

with_bot.linear_order = {le := partial_order.le with_bot.partial_order, lt := partial_order.lt with_bot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _}

source

@[instance]

def with_bot.decidable_lt {α : Type u} [has_lt α] [decidable_rel has_lt.lt] :

decidable_rel has_lt.lt

Equations

with_bot.decidable_lt (option.some x) (option.some y) = dite (x < y) (λ (h : x < y), decidable.is_true _) (λ (h : ¬x < y), decidable.is_false _)
with_bot.decidable_lt (option.some val) option.none = decidable.is_false _
with_bot.decidable_lt option.none (option.some x) = decidable.is_true _
with_bot.decidable_lt option.none option.none = decidable.is_false with_bot.decidable_lt._main._proof_1

source

@[instance]

def with_bot.decidable_linear_order {α : Type u} [decidable_linear_order α] :

decidable_linear_order (with_bot α)

Equations

with_bot.decidable_linear_order = {le := linear_order.le with_bot.linear_order, lt := linear_order.lt with_bot.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (a b : with_bot α), option.cases_on a (decidable.is_true _) (λ (a : α), option.cases_on b (decidable.is_false _) (λ (b : α), decidable_of_iff (option.some (option.some a) ≤ option.some (option.some b)) _)), decidable_eq := decidable_eq_of_decidable_le (λ (a b : with_bot α), option.cases_on a (decidable.is_true _) (λ (a : α), option.cases_on b (decidable.is_false _) (λ (b : α), decidable_of_iff (option.some (option.some a) ≤ option.some (option.some b)) _))), decidable_lt := decidable_lt_of_decidable_le (λ (a b : with_bot α), option.cases_on a (decidable.is_true _) (λ (a : α), option.cases_on b (decidable.is_false _) (λ (b : α), decidable_of_iff (option.some (option.some a) ≤ option.some (option.some b)) _)))}

source

@[instance]

def with_bot.semilattice_sup {α : Type u} [semilattice_sup α] :

semilattice_sup_bot (with_bot α)

Equations

with_bot.semilattice_sup = {bot := order_bot.bot with_bot.order_bot, le := order_bot.le with_bot.order_bot, lt := order_bot.lt with_bot.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := option.lift_or_get has_sup.sup, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def with_bot.semilattice_inf {α : Type u} [semilattice_inf α] :

semilattice_inf_bot (with_bot α)

Equations

with_bot.semilattice_inf = {bot := order_bot.bot with_bot.order_bot, le := order_bot.le with_bot.order_bot, lt := order_bot.lt with_bot.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := λ (o₁ o₂ : with_bot α), option.bind o₁ (λ (a : α), option.map (λ (b : α), a ⊓ b) o₂), inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def with_bot.lattice {α : Type u} [lattice α] :

lattice (with_bot α)

Equations

with_bot.lattice = {sup := semilattice_sup_bot.sup with_bot.semilattice_sup, le := semilattice_sup_bot.le with_bot.semilattice_sup, lt := semilattice_sup_bot.lt with_bot.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf_bot.inf with_bot.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

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

with_bot.order_top = {top := option.some ⊤, le := partial_order.le with_bot.partial_order, lt := partial_order.lt with_bot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}

source

@[instance]

def with_bot.bounded_lattice {α : Type u} [bounded_lattice α] :

bounded_lattice (with_bot α)

Equations

with_bot.bounded_lattice = {sup := lattice.sup with_bot.lattice, le := lattice.le with_bot.lattice, lt := lattice.lt with_bot.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf with_bot.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top with_bot.order_top, le_top := _, bot := order_bot.bot with_bot.order_bot, bot_le := _}

source

theorem with_bot.well_founded_lt {α : Type u} [partial_order α] :

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 α)

Equations

with_bot.densely_ordered = _
_ = _
_ = _
_ = _
_ = _
_ = _
_ = _

source

def with_top :

Type u_1 → Type u_1

Equations

with_top α = option α

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

with_top.has_coe_t = {coe := option.some α}

source

@[instance]

def with_top.has_top {α : Type u} :

has_top (with_top α)

Equations

with_top.has_top = {top := option.none α}

source

@[instance]

def with_top.inhabited {α : Type u} :

inhabited (with_top α)

Equations

with_top.inhabited = {default := ⊤}

source

theorem with_top.none_eq_top {α : Type u} :

option.none = ⊤

source

theorem with_top.some_eq_coe {α : Type u} (a : α) :

option.some a = ↑a

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

with_top.has_lt = {lt := λ (o₁ o₂ : option α), ∃ (b : α) (H : b ∈ o₁), ∀ (a : α), a ∈ o₂ → b < a}

source

@[instance]

def with_top.has_le {α : Type u} [has_le α] :

has_le (with_top α)

Equations

with_top.has_le = {le := λ (o₁ o₂ : option α), ∀ (a : α), a ∈ o₂ → (∃ (b : α) (H : b ∈ o₁), b ≤ a)}

source

@[simp]

theorem with_top.some_lt_some {α : Type u} [has_lt α] {a b : α} :

option.some a < option.some b ↔ a < b

source

@[simp]

theorem with_top.some_le_some {α : Type u} [has_le α] {a b : α} :

option.some a ≤ option.some b ↔ a ≤ b

source

@[simp]

theorem with_top.none_le {α : Type u} [has_le α] {a : with_top α} :

a ≤ option.none

source

@[simp]

theorem with_top.none_lt_some {α : Type u} [has_lt α] {a : α} :

option.some a < option.none

source

@[instance]

def with_top.preorder {α : Type u} [preorder α] :

preorder (with_top α)

Equations

with_top.preorder = {le := λ (o₁ o₂ : option α), ∀ (a : α), a ∈ o₂ → (∃ (b : α) (H : b ∈ o₁), b ≤ a), lt := has_lt.lt with_top.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

source

@[instance]

def with_top.partial_order {α : Type u} [partial_order α] :

partial_order (with_top α)

Equations

with_top.partial_order = {le := preorder.le with_top.preorder, lt := preorder.lt with_top.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[instance]

def with_top.order_top {α : Type u} [partial_order α] :

order_top (with_top α)

Equations

with_top.order_top = {top := ⊤, le := partial_order.le with_top.partial_order, lt := partial_order.lt with_top.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}

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 ∈ 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

with_top.linear_order = {le := partial_order.le with_top.partial_order, lt := partial_order.lt with_top.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _}

source

@[instance]

def with_top.decidable_linear_order {α : Type u} [decidable_linear_order α] :

decidable_linear_order (with_top α)

Equations

with_top.decidable_linear_order = {le := linear_order.le with_top.linear_order, lt := linear_order.lt with_top.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (a b : with_top α), option.cases_on b (decidable.is_true _) (λ (b : α), option.cases_on a (decidable.is_false _) (λ (a : α), decidable_of_iff (option.some (option.some a) ≤ option.some (option.some b)) _)), decidable_eq := decidable_eq_of_decidable_le (λ (a b : with_top α), option.cases_on b (decidable.is_true _) (λ (b : α), option.cases_on a (decidable.is_false _) (λ (a : α), decidable_of_iff (option.some (option.some a) ≤ option.some (option.some b)) _))), decidable_lt := decidable_lt_of_decidable_le (λ (a b : with_top α), option.cases_on b (decidable.is_true _) (λ (b : α), option.cases_on a (decidable.is_false _) (λ (a : α), decidable_of_iff (option.some (option.some a) ≤ option.some (option.some b)) _)))}

source

@[instance]

def with_top.semilattice_inf {α : Type u} [semilattice_inf α] :

semilattice_inf_top (with_top α)

Equations

with_top.semilattice_inf = {top := order_top.top with_top.order_top, le := order_top.le with_top.order_top, lt := order_top.lt with_top.order_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, inf := option.lift_or_get has_inf.inf, inf_le_left := _, inf_le_right := _, le_inf := _}

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

with_top.semilattice_sup = {top := order_top.top with_top.order_top, le := order_top.le with_top.order_top, lt := order_top.lt with_top.order_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := λ (o₁ o₂ : with_top α), option.bind o₁ (λ (a : α), option.map (λ (b : α), a ⊔ b) o₂), le_sup_left := _, le_sup_right := _, sup_le := _}

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

with_top.lattice = {sup := semilattice_sup_top.sup with_top.semilattice_sup, le := semilattice_sup_top.le with_top.semilattice_sup, lt := semilattice_sup_top.lt with_top.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf_top.inf with_top.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

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

with_top.order_bot = {bot := option.some ⊥, le := partial_order.le with_top.partial_order, lt := partial_order.lt with_top.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}

source

@[instance]

def with_top.bounded_lattice {α : Type u} [bounded_lattice α] :

bounded_lattice (with_top α)

Equations

with_top.bounded_lattice = {sup := lattice.sup with_top.lattice, le := lattice.le with_top.lattice, lt := lattice.lt with_top.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf with_top.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top with_top.order_top, le_top := _, bot := order_bot.bot with_top.order_bot, bot_le := _}

source

theorem with_top.well_founded_lt {α : Type u_1} [partial_order α] :

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 α)

Equations

with_top.densely_ordered = _
_ = _
_ = _
_ = _
_ = _
_ = _

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} :

(∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) → semilattice_sup {x // P x}

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

Equations

subtype.semilattice_sup Psup = {sup := λ (x y : {x // P x}), ⟨x.val ⊔ y.val, _⟩, le := partial_order.le (subtype.partial_order P), lt := partial_order.lt (subtype.partial_order P), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

def subtype.semilattice_inf {α : Type u} [semilattice_inf α] {P : α → Prop} :

(∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) → semilattice_inf {x // P x}

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

Equations

subtype.semilattice_inf Pinf = {inf := λ (x y : {x // P x}), ⟨x.val ⊓ y.val, _⟩, le := partial_order.le (subtype.partial_order P), lt := partial_order.lt (subtype.partial_order P), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

source

def subtype.semilattice_sup_bot {α : Type u} [semilattice_sup_bot α] {P : α → Prop} :

P ⊥ → (∀ ⦃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

subtype.semilattice_sup_bot Pbot Psup = {bot := ⟨⊥, Pbot⟩, le := semilattice_sup.le (subtype.semilattice_sup Psup), lt := semilattice_sup.lt (subtype.semilattice_sup Psup), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := semilattice_sup.sup (subtype.semilattice_sup Psup), le_sup_left := _, le_sup_right := _, sup_le := _}

source

def subtype.semilattice_inf_bot {α : Type u} [semilattice_inf_bot α] {P : α → Prop} :

P ⊥ → (∀ ⦃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

subtype.semilattice_inf_bot Pbot Pinf = {bot := ⟨⊥, Pbot⟩, le := semilattice_inf.le (subtype.semilattice_inf Pinf), lt := semilattice_inf.lt (subtype.semilattice_inf Pinf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := semilattice_inf.inf (subtype.semilattice_inf Pinf), inf_le_left := _, inf_le_right := _, le_inf := _}

source

def subtype.semilattice_inf_top {α : Type u} [semilattice_inf_top α] {P : α → Prop} :

P ⊤ → (∀ ⦃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

subtype.semilattice_inf_top Ptop Pinf = {top := ⟨⊤, Ptop⟩, le := semilattice_inf.le (subtype.semilattice_inf Pinf), lt := semilattice_inf.lt (subtype.semilattice_inf Pinf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, inf := semilattice_inf.inf (subtype.semilattice_inf Pinf), inf_le_left := _, inf_le_right := _, le_inf := _}

source

def subtype.lattice {α : Type u} [lattice α] {P : α → Prop} :

(∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) → (∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) → lattice {x // P x}

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

Equations

subtype.lattice Psup Pinf = {sup := semilattice_sup.sup (subtype.semilattice_sup Psup), le := semilattice_inf.le (subtype.semilattice_inf Pinf), lt := semilattice_inf.lt (subtype.semilattice_inf Pinf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf (subtype.semilattice_inf Pinf), inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def order_dual.has_top (α : Type u) [has_bot α] :

has_top (order_dual α)

Equations

order_dual.has_top α = {top := ⊥}

source

@[instance]

def order_dual.has_bot (α : Type u) [has_top α] :

has_bot (order_dual α)

Equations

order_dual.has_bot α = {bot := ⊤}

source

@[instance]

def order_dual.order_top (α : Type u) [order_bot α] :

order_top (order_dual α)

Equations

order_dual.order_top α = {top := ⊤, le := partial_order.le (order_dual.partial_order α), lt := partial_order.lt (order_dual.partial_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}

source

@[instance]

def order_dual.order_bot (α : Type u) [order_top α] :

order_bot (order_dual α)

Equations

order_dual.order_bot α = {bot := ⊥, le := partial_order.le (order_dual.partial_order α), lt := partial_order.lt (order_dual.partial_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}

source

@[instance]

def order_dual.semilattice_sup_top (α : Type u) [semilattice_inf_bot α] :

semilattice_sup_top (order_dual α)

Equations

order_dual.semilattice_sup_top α = {top := order_top.top (order_dual.order_top α), le := semilattice_sup.le (order_dual.semilattice_sup α), lt := semilattice_sup.lt (order_dual.semilattice_sup α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := semilattice_sup.sup (order_dual.semilattice_sup α), le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def order_dual.semilattice_sup_bot (α : Type u) [semilattice_inf_top α] :

semilattice_sup_bot (order_dual α)

Equations

order_dual.semilattice_sup_bot α = {bot := order_bot.bot (order_dual.order_bot α), le := semilattice_sup.le (order_dual.semilattice_sup α), lt := semilattice_sup.lt (order_dual.semilattice_sup α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := semilattice_sup.sup (order_dual.semilattice_sup α), le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def order_dual.semilattice_inf_top (α : Type u) [semilattice_sup_bot α] :

semilattice_inf_top (order_dual α)

Equations

order_dual.semilattice_inf_top α = {top := order_top.top (order_dual.order_top α), le := semilattice_inf.le (order_dual.semilattice_inf α), lt := semilattice_inf.lt (order_dual.semilattice_inf α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, inf := semilattice_inf.inf (order_dual.semilattice_inf α), inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def order_dual.semilattice_inf_bot (α : Type u) [semilattice_sup_top α] :

semilattice_inf_bot (order_dual α)

Equations

order_dual.semilattice_inf_bot α = {bot := order_bot.bot (order_dual.order_bot α), le := semilattice_inf.le (order_dual.semilattice_inf α), lt := semilattice_inf.lt (order_dual.semilattice_inf α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := semilattice_inf.inf (order_dual.semilattice_inf α), inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def order_dual.bounded_lattice (α : Type u) [bounded_lattice α] :

bounded_lattice (order_dual α)

Equations

order_dual.bounded_lattice α = {sup := lattice.sup (order_dual.lattice α), le := lattice.le (order_dual.lattice α), lt := lattice.lt (order_dual.lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf (order_dual.lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top (order_dual.order_top α), le_top := _, bot := order_bot.bot (order_dual.order_bot α), bot_le := _}

source

@[instance]

def order_dual.bounded_distrib_lattice (α : Type u) [bounded_distrib_lattice α] :

bounded_distrib_lattice (order_dual α)

Equations

order_dual.bounded_distrib_lattice α = {sup := bounded_lattice.sup (order_dual.bounded_lattice α), le := bounded_lattice.le (order_dual.bounded_lattice α), lt := bounded_lattice.lt (order_dual.bounded_lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf (order_dual.bounded_lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, top := bounded_lattice.top (order_dual.bounded_lattice α), le_top := _, bot := bounded_lattice.bot (order_dual.bounded_lattice α), bot_le := _}

source

@[instance]

def prod.has_top (α : Type u) (β : Type v) [has_top α] [has_top β] :

has_top (α × β)

Equations

prod.has_top α β = {top := (⊤, ⊤)}

source

@[instance]

def prod.has_bot (α : Type u) (β : Type v) [has_bot α] [has_bot β] :

has_bot (α × β)

Equations

prod.has_bot α β = {bot := (⊥, ⊥)}

source

@[instance]

def prod.order_top (α : Type u) (β : Type v) [order_top α] [order_top β] :

order_top (α × β)

Equations

prod.order_top α β = {top := ⊤, le := partial_order.le (prod.partial_order α β), lt := partial_order.lt (prod.partial_order α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}

source

@[instance]

def prod.order_bot (α : Type u) (β : Type v) [order_bot α] [order_bot β] :

order_bot (α × β)

Equations

prod.order_bot α β = {bot := ⊥, le := partial_order.le (prod.partial_order α β), lt := partial_order.lt (prod.partial_order α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}

source

@[instance]

def prod.semilattice_sup_top (α : Type u) (β : Type v) [semilattice_sup_top α] [semilattice_sup_top β] :

semilattice_sup_top (α × β)

Equations

prod.semilattice_sup_top α β = {top := order_top.top (prod.order_top α β), le := semilattice_sup.le (prod.semilattice_sup α β), lt := semilattice_sup.lt (prod.semilattice_sup α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := semilattice_sup.sup (prod.semilattice_sup α β), le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def prod.semilattice_inf_top (α : Type u) (β : Type v) [semilattice_inf_top α] [semilattice_inf_top β] :

semilattice_inf_top (α × β)

Equations

prod.semilattice_inf_top α β = {top := order_top.top (prod.order_top α β), le := semilattice_inf.le (prod.semilattice_inf α β), lt := semilattice_inf.lt (prod.semilattice_inf α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, inf := semilattice_inf.inf (prod.semilattice_inf α β), inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def prod.semilattice_sup_bot (α : Type u) (β : Type v) [semilattice_sup_bot α] [semilattice_sup_bot β] :

semilattice_sup_bot (α × β)

Equations

prod.semilattice_sup_bot α β = {bot := order_bot.bot (prod.order_bot α β), le := semilattice_sup.le (prod.semilattice_sup α β), lt := semilattice_sup.lt (prod.semilattice_sup α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := semilattice_sup.sup (prod.semilattice_sup α β), le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def prod.semilattice_inf_bot (α : Type u) (β : Type v) [semilattice_inf_bot α] [semilattice_inf_bot β] :

semilattice_inf_bot (α × β)

Equations

prod.semilattice_inf_bot α β = {bot := order_bot.bot (prod.order_bot α β), le := semilattice_inf.le (prod.semilattice_inf α β), lt := semilattice_inf.lt (prod.semilattice_inf α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := semilattice_inf.inf (prod.semilattice_inf α β), inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def prod.bounded_lattice (α : Type u) (β : Type v) [bounded_lattice α] [bounded_lattice β] :

bounded_lattice (α × β)

Equations

prod.bounded_lattice α β = {sup := lattice.sup (prod.lattice α β), le := lattice.le (prod.lattice α β), lt := lattice.lt (prod.lattice α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf (prod.lattice α β), inf_le_left := _, inf_le_right := _, le_inf := _, top := order_top.top (prod.order_top α β), le_top := _, bot := order_bot.bot (prod.order_bot α β), bot_le := _}

source

@[instance]

def prod.bounded_distrib_lattice (α : Type u) (β : Type v) [bounded_distrib_lattice α] [bounded_distrib_lattice β] :

bounded_distrib_lattice (α × β)

Equations

prod.bounded_distrib_lattice α β = {sup := bounded_lattice.sup (prod.bounded_lattice α β), le := bounded_lattice.le (prod.bounded_lattice α β), lt := bounded_lattice.lt (prod.bounded_lattice α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := bounded_lattice.inf (prod.bounded_lattice α β), inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, top := bounded_lattice.top (prod.bounded_lattice α β), le_top := _, bot := bounded_lattice.bot (prod.bounded_lattice α β), bot_le := _}

source

def disjoint {α : Type u} [semilattice_inf_bot α] :

α → α → 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

disjoint a b = (a ⊓ b ≤ ⊥)

source

theorem disjoint.eq_bot {α : Type u} [semilattice_inf_bot α] {a b : α} :

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 : α} :

a ≤ b → c ≤ d → disjoint b d → disjoint a c

source

theorem disjoint.mono_left {α : Type u} [semilattice_inf_bot α] {a b c : α} :

a ≤ b → disjoint b c → disjoint a c

source

theorem disjoint.mono_right {α : Type u} [semilattice_inf_bot α] {a b c : α} :

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 : α} :

a ≠ ⊥ → 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 : α} :

disjoint a c → disjoint b c → disjoint (a ⊔ b) c

source

theorem disjoint.sup_right {α : Type u} [bounded_distrib_lattice α] {a b c : α} :

disjoint a b → disjoint a c → disjoint a (b ⊔ c)

source

structure is_compl {α : Type u} [bounded_lattice α] :

α → α → Prop

inf_le_bot : x ⊓ y ≤ ⊥
top_le_sup : ⊤ ≤ x ⊔ y

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 : α} :

is_compl x y → disjoint x y

source

theorem is_compl.symm {α : Type u} [bounded_lattice α] {x y : α} :

is_compl x y → is_compl y x

source

theorem is_compl.of_eq {α : Type u} [bounded_lattice α] {x y : α} :

x ⊓ y = ⊥ → x ⊔ y = ⊤ → is_compl x y

source

theorem is_compl.inf_eq_bot {α : Type u} [bounded_lattice α] {x y : α} :

is_compl x y → x ⊓ y = ⊥

source

theorem is_compl.sup_eq_top {α : Type u} [bounded_lattice α] {x y : α} :

is_compl x y → x ⊔ y = ⊤

source

theorem is_compl.to_order_dual {α : Type u} [bounded_lattice α] {x y : α} :

is_compl x y → is_compl x y

source

theorem is_compl.le_left_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :

is_compl x y → (z ≤ x ↔ disjoint z y)

source

theorem is_compl.le_right_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :

is_compl x y → (z ≤ y ↔ disjoint z x)

source

theorem is_compl.left_le_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :

is_compl x y → (x ≤ z ↔ ⊤ ≤ z ⊔ y)

source

theorem is_compl.right_le_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :

is_compl x y → (y ≤ z ↔ ⊤ ≤ z ⊔ x)

source

theorem is_compl.antimono {α : Type u} [bounded_distrib_lattice α] {x y x' y' : α} :

is_compl x y → is_compl x' y' → x ≤ x' → y' ≤ y

source

theorem is_compl.right_unique {α : Type u} [bounded_distrib_lattice α] {x y z : α} :

is_compl x y → is_compl x z → y = z

source

theorem is_compl.left_unique {α : Type u} [bounded_distrib_lattice α] {x y z : α} :

is_compl x z → is_compl y z → x = y

source

theorem is_compl.sup_inf {α : Type u} [bounded_distrib_lattice α] {x y x' y' : α} :

is_compl x y → 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' : α} :

is_compl x y → 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 : α} :

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 : α} :

is_compl y z → (x ⊓ z = ⊥ ↔ x ≤ y)

source

theorem is_compl.disjoint_left_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :

is_compl y z → (disjoint x y ↔ x ≤ z)

source

theorem is_compl.disjoint_right_iff {α : Type u} [bounded_distrib_lattice α] {x y z : α} :

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 ⊤ ⊥

mathlib documentation

order.bounded_lattice

`is_compl` predicate

General documentation

Additional documentation

Library

mathlib documentation

order.​bounded_lattice

is_compl predicate

General documentation

Additional documentation

Library

order.bounded_lattice

`is_compl` predicate