mathlib docs: order.lattice

source

@[instance]

def set.Ico.semilattice_inf {α : Type u_1} {a b : α} [semilattice_inf α] :

semilattice_inf ↥(set.Ico a b)

Equations

set.Ico.semilattice_inf = subtype.semilattice_inf set.Ico.semilattice_inf._proof_1

source

def set.Ico.order_bot {α : Type u_1} {a b : α} [partial_order α] (h : a < b) :

order_bot ↥(set.Ico a b)

Ico a b has a bottom element whenever a < b.

Equations

set.Ico.order_bot h = {bot := ⟨a, _⟩, le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ set.Ico a b)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ set.Ico a b)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}

source

def set.Ico.semilattice_inf_bot {α : Type u_1} {a b : α} [semilattice_inf α] (h : a < b) :

semilattice_inf_bot ↥(set.Ico a b)

Ico a b is a semilattice_inf_bot whenever a < b.

Equations

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

source

@[instance]

def set.Iio.semilattice_inf {α : Type u_1} [semilattice_inf α] {a : α} :

semilattice_inf ↥(set.Iio a)

Equations

set.Iio.semilattice_inf = subtype.semilattice_inf set.Iio.semilattice_inf._proof_1

source

@[instance]

def set.Ioc.semilattice_sup {α : Type u_1} {a b : α} [semilattice_sup α] :

semilattice_sup ↥(set.Ioc a b)

Equations

set.Ioc.semilattice_sup = subtype.semilattice_sup set.Ioc.semilattice_sup._proof_1

source

def set.Ioc.order_top {α : Type u_1} {a b : α} [partial_order α] (h : a < b) :

order_top ↥(set.Ioc a b)

Ioc a b has a top element whenever a < b.

Equations

set.Ioc.order_top h = {top := ⟨b, _⟩, le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ set.Ioc a b)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ set.Ioc a b)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}

source

def set.Ioc.semilattice_sup_top {α : Type u_1} {a b : α} [semilattice_sup α] (h : a < b) :

semilattice_sup_top ↥(set.Ioc a b)

Ioc a b is a semilattice_sup_top whenever a < b.

Equations

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

source

@[instance]

def set.Iio.set.Ioi.semilattice_sup {α : Type u_1} [semilattice_sup α] {a : α} :

semilattice_sup ↥(set.Ioi a)

Equations

set.Iio.set.Ioi.semilattice_sup = subtype.semilattice_sup set.Iio.set.Ioi.semilattice_sup._proof_1

source

@[instance]

def set.Iic.semilattice_inf {α : Type u_1} {a : α} [semilattice_inf α] :

semilattice_inf ↥(set.Iic a)

Equations

set.Iic.semilattice_inf = subtype.semilattice_inf set.Iic.semilattice_inf._proof_1

source

@[instance]

def set.Iic.semilattice_sup {α : Type u_1} {a : α} [semilattice_sup α] :

semilattice_sup ↥(set.Iic a)

Equations

set.Iic.semilattice_sup = subtype.semilattice_sup set.Iic.semilattice_sup._proof_1

source

@[instance]

def set.Iic.lattice {α : Type u_1} {a : α} [lattice α] :

lattice ↥(set.Iic a)

Equations

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

source

@[instance]

def set.Iic.order_top {α : Type u_1} {a : α} [partial_order α] :

order_top ↥(set.Iic a)

Equations

set.Iic.order_top = {top := ⟨a, _⟩, le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ set.Iic a)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ set.Iic a)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}

source

@[simp]

theorem set.Iic.coe_top {α : Type u_1} [partial_order α] {a : α} :

↑⊤ = a

source

@[instance]

def set.Iic.semilattice_inf_top {α : Type u_1} {a : α} [semilattice_inf α] :

semilattice_inf_top ↥(set.Iic a)

Equations

set.Iic.semilattice_inf_top = {top := order_top.top set.Iic.order_top, le := semilattice_inf.le set.Iic.semilattice_inf, lt := semilattice_inf.lt set.Iic.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, inf := semilattice_inf.inf set.Iic.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def set.Iic.semilattice_sup_top {α : Type u_1} {a : α} [semilattice_sup α] :

semilattice_sup_top ↥(set.Iic a)

Equations

set.Iic.semilattice_sup_top = {top := order_top.top set.Iic.order_top, le := semilattice_sup.le set.Iic.semilattice_sup, lt := semilattice_sup.lt set.Iic.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := semilattice_sup.sup set.Iic.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def set.Iic.order_bot {α : Type u_1} {a : α} [order_bot α] :

order_bot ↥(set.Iic a)

Equations

set.Iic.order_bot = {bot := ⟨⊥, _⟩, le := partial_order.le infer_instance, lt := partial_order.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}

source

@[simp]

theorem set.Iic.coe_bot {α : Type u_1} [order_bot α] {a : α} :

↑⊥ = ⊥

source

@[instance]

def set.Iic.semilattice_inf_bot {α : Type u_1} {a : α} [semilattice_inf_bot α] :

semilattice_inf_bot ↥(set.Iic a)

Equations

set.Iic.semilattice_inf_bot = {bot := order_bot.bot set.Iic.order_bot, le := semilattice_inf.le set.Iic.semilattice_inf, lt := semilattice_inf.lt set.Iic.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := semilattice_inf.inf set.Iic.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def set.Iic.semilattice_sup_bot {α : Type u_1} {a : α} [semilattice_sup_bot α] :

semilattice_sup_bot ↥(set.Iic a)

Equations

set.Iic.semilattice_sup_bot = {bot := order_bot.bot set.Iic.order_bot, le := semilattice_sup.le set.Iic.semilattice_sup, lt := semilattice_sup.lt set.Iic.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := semilattice_sup.sup set.Iic.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def set.Iic.bounded_lattice {α : Type u_1} {a : α} [bounded_lattice α] :

bounded_lattice ↥(set.Iic a)

Equations

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

source

@[instance]

def set.Ici.semilattice_inf {α : Type u_1} {a : α} [semilattice_inf α] :

semilattice_inf ↥(set.Ici a)

Equations

set.Ici.semilattice_inf = subtype.semilattice_inf set.Ici.semilattice_inf._proof_1

source

@[instance]

def set.Ici.semilattice_sup {α : Type u_1} {a : α} [semilattice_sup α] :

semilattice_sup ↥(set.Ici a)

Equations

set.Ici.semilattice_sup = subtype.semilattice_sup set.Ici.semilattice_sup._proof_1

source

@[instance]

def set.Ici.lattice {α : Type u_1} {a : α} [lattice α] :

lattice ↥(set.Ici a)

Equations

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

source

@[instance]

def set.Ici.order_bot {α : Type u_1} {a : α} [partial_order α] :

order_bot ↥(set.Ici a)

Equations

set.Ici.order_bot = {bot := ⟨a, _⟩, le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ set.Ici a)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ set.Ici a)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}

source

@[simp]

theorem set.Ici.coe_bot {α : Type u_1} [partial_order α] {a : α} :

↑⊥ = a

source

@[instance]

def set.Ici.semilattice_inf_bot {α : Type u_1} {a : α} [semilattice_inf α] :

semilattice_inf_bot ↥(set.Ici a)

Equations

set.Ici.semilattice_inf_bot = {bot := order_bot.bot set.Ici.order_bot, le := semilattice_inf.le set.Ici.semilattice_inf, lt := semilattice_inf.lt set.Ici.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, inf := semilattice_inf.inf set.Ici.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def set.Ici.semilattice_sup_bot {α : Type u_1} {a : α} [semilattice_sup α] :

semilattice_sup_bot ↥(set.Ici a)

Equations

set.Ici.semilattice_sup_bot = {bot := order_bot.bot set.Ici.order_bot, le := semilattice_sup.le set.Ici.semilattice_sup, lt := semilattice_sup.lt set.Ici.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _, sup := semilattice_sup.sup set.Ici.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def set.Ici.order_top {α : Type u_1} {a : α} [order_top α] :

order_top ↥(set.Ici a)

Equations

set.Ici.order_top = {top := ⟨⊤, _⟩, le := partial_order.le infer_instance, lt := partial_order.lt infer_instance, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}

source

@[simp]

theorem set.Ici.coe_top {α : Type u_1} [order_top α] {a : α} :

↑⊤ = ⊤

source

@[instance]

def set.Ici.semilattice_sup_top {α : Type u_1} {a : α} [semilattice_sup_top α] :

semilattice_sup_top ↥(set.Ici a)

Equations

set.Ici.semilattice_sup_top = {top := order_top.top set.Ici.order_top, le := semilattice_sup.le set.Ici.semilattice_sup, lt := semilattice_sup.lt set.Ici.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := semilattice_sup.sup set.Ici.semilattice_sup, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def set.Ici.semilattice_inf_top {α : Type u_1} {a : α} [semilattice_inf_top α] :

semilattice_inf_top ↥(set.Ici a)

Equations

set.Ici.semilattice_inf_top = {top := order_top.top set.Ici.order_top, le := semilattice_inf.le set.Ici.semilattice_inf, lt := semilattice_inf.lt set.Ici.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, inf := semilattice_inf.inf set.Ici.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[instance]

def set.Ici.bounded_lattice {α : Type u_1} {a : α} [bounded_lattice α] :

bounded_lattice ↥(set.Ici a)

Equations

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

source

@[instance]

def set.Icc.semilattice_inf {α : Type u_1} [semilattice_inf α] {a b : α} :

semilattice_inf ↥(set.Icc a b)

Equations

set.Icc.semilattice_inf = subtype.semilattice_inf set.Icc.semilattice_inf._proof_1

source

@[instance]

def set.Icc.semilattice_sup {α : Type u_1} [semilattice_sup α] {a b : α} :

semilattice_sup ↥(set.Icc a b)

Equations

set.Icc.semilattice_sup = subtype.semilattice_sup set.Icc.semilattice_sup._proof_1

source

@[instance]

def set.Icc.lattice {α : Type u_1} [lattice α] {a b : α} :

lattice ↥(set.Icc a b)

Equations

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

source

def set.Icc.order_bot {α : Type u_1} [partial_order α] {a b : α} (h : a ≤ b) :

order_bot ↥(set.Icc a b)

Icc a b has a bottom element whenever a ≤ b.

Equations

set.Icc.order_bot h = {bot := ⟨a, _⟩, le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ set.Icc a b)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ set.Icc a b)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}

source

def set.Icc.order_top {α : Type u_1} [partial_order α] {a b : α} (h : a ≤ b) :

order_top ↥(set.Icc a b)

Icc a b has a top element whenever a ≤ b.

Equations

set.Icc.order_top h = {top := ⟨b, _⟩, le := partial_order.le (subtype.partial_order (λ (x : α), x ∈ set.Icc a b)), lt := partial_order.lt (subtype.partial_order (λ (x : α), x ∈ set.Icc a b)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}

source

def set.Icc.semilattice_inf_bot {α : Type u_1} [semilattice_inf α] {a b : α} (h : a ≤ b) :

semilattice_inf_bot ↥(set.Icc a b)

Icc a b is a semilattice_inf_bot whenever a ≤ b.

Equations

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

source

def set.Icc.semilattice_inf_top {α : Type u_1} [semilattice_inf α] {a b : α} (h : a ≤ b) :

semilattice_inf_top ↥(set.Icc a b)

Icc a b is a semilattice_inf_top whenever a ≤ b.

Equations

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

source

def set.Icc.semilattice_sup_bot {α : Type u_1} [semilattice_sup α] {a b : α} (h : a ≤ b) :

semilattice_sup_bot ↥(set.Icc a b)

Icc a b is a semilattice_sup_bot whenever a ≤ b.

Equations

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

source

def set.Icc.semilattice_sup_top {α : Type u_1} [semilattice_sup α] {a b : α} (h : a ≤ b) :

semilattice_sup_top ↥(set.Icc a b)

Icc a b is a semilattice_sup_top whenever a ≤ b.

Equations

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

source

def set.Icc.bounded_lattice {α : Type u_1} [lattice α] {a b : α} (h : a ≤ b) :

bounded_lattice ↥(set.Icc a b)

Icc a b is a bounded_lattice whenever a ≤ b.

Equations

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

mathlib documentation

Intervals in Lattices #

Main definitions #