Documentation

Mathlib.Order.LatticeIntervals

Intervals in Lattices #

In this file, we provide instances of lattice structures on intervals within lattices. Some of them depend on the order of the endpoints of the interval, and thus are not made global instances. These are probably not all of the lattice instances that could be placed on these intervals, but more can be added easily along the same lines when needed.

Main definitions #

In the following, * can represent either c, o, or i.

Set.Ic*.orderBot
Set.Ii*.semillaticeInf
Set.I*c.orderTop
Set.I*c.semillaticeInf
Set.I**.lattice
Set.Iic.boundedOrder, within an OrderBot
Set.Ici.boundedOrder, within an OrderTop

instance Set.Ico.semilatticeInf {α : Type u_1} [inst : SemilatticeInf α] {a : α} {b : α} :

SemilatticeInf ↑(Set.Ico a b)

Equations

Set.Ico.semilatticeInf = Subtype.semilatticeInf (_ : ∀ (x x_1 : α), x ∈ Set.Ico a b → x_1 ∈ Set.Ico a b → a ≤ x ⊓ x_1 ∧ x ⊓ x_1 < b)

def Set.Ico.orderBot {α : Type u_1} [inst : PartialOrder α] {a : α} {b : α} (h : a < b) :

OrderBot ↑(Set.Ico a b)

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

Equations

Set.Ico.orderBot h = IsLeast.orderBot (_ : IsLeast (Set.Ico a b) a)

instance Set.Iio.semilatticeInf {α : Type u_1} [inst : SemilatticeInf α] {a : α} :

SemilatticeInf ↑(Set.Iio a)

Equations

Set.Iio.semilatticeInf = Subtype.semilatticeInf (_ : ∀ (x x_1 : α), x ∈ Set.Iio a → x_1 ∈ Set.Iio a → x ⊓ x_1 < a)

instance Set.Ioc.semilatticeSup {α : Type u_1} [inst : SemilatticeSup α] {a : α} {b : α} :

SemilatticeSup ↑(Set.Ioc a b)

Equations

Set.Ioc.semilatticeSup = Subtype.semilatticeSup (_ : ∀ (x x_1 : α), x ∈ Set.Ioc a b → x_1 ∈ Set.Ioc a b → a < x ⊔ x_1 ∧ x ⊔ x_1 ≤ b)

def Set.Ioc.orderTop {α : Type u_1} [inst : PartialOrder α] {a : α} {b : α} (h : a < b) :

OrderTop ↑(Set.Ioc a b)

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

Equations

Set.Ioc.orderTop h = IsGreatest.orderTop (_ : IsGreatest (Set.Ioc a b) b)

instance Set.Ioi.semilatticeSup {α : Type u_1} [inst : SemilatticeSup α] {a : α} :

SemilatticeSup ↑(Set.Ioi a)

Equations

Set.Ioi.semilatticeSup = Subtype.semilatticeSup (_ : ∀ (x x_1 : α), x ∈ Set.Ioi a → x_1 ∈ Set.Ioi a → a < x ⊔ x_1)

instance Set.Iic.semilatticeInf {α : Type u_1} [inst : SemilatticeInf α] {a : α} :

SemilatticeInf ↑(Set.Iic a)

Equations

Set.Iic.semilatticeInf = Subtype.semilatticeInf (_ : ∀ (x x_1 : α), x ∈ Set.Iic a → x_1 ∈ Set.Iic a → x ⊓ x_1 ≤ a)

instance Set.Iic.semilatticeSup {α : Type u_1} [inst : SemilatticeSup α] {a : α} :

SemilatticeSup ↑(Set.Iic a)

Equations

Set.Iic.semilatticeSup = Subtype.semilatticeSup (_ : ∀ (x x_1 : α), x ∈ Set.Iic a → x_1 ∈ Set.Iic a → x ⊔ x_1 ≤ a)

instance Set.Iic.instLatticeElemIicToPreorderToPartialOrderToSemilatticeInf {α : Type u_1} [inst : Lattice α] {a : α} :

Lattice ↑(Set.Iic a)

Equations

One or more equations did not get rendered due to their size.

instance Set.Iic.orderTop {α : Type u_1} [inst : Preorder α] {a : α} :

OrderTop ↑(Set.Iic a)

Equations

Set.Iic.orderTop = OrderTop.mk (_ : ∀ (x : ↑(Set.Iic a)), ↑x ∈ Set.Iic a)

@[simp]

theorem Set.Iic.coe_top {α : Type u_1} [inst : Preorder α] {a : α} :

↑⊤ = a

instance Set.Iic.orderBot {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] {a : α} :

OrderBot ↑(Set.Iic a)

Equations

Set.Iic.orderBot = OrderBot.mk (_ : ∀ (x : ↑(Set.Iic a)), ⊥ ≤ x)

@[simp]

theorem Set.Iic.coe_bot {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] {a : α} :

instance Set.Iic.instBoundedOrderElemIicLeToLEMemSetInstMembershipSet {α : Type u_1} [inst : Preorder α] [inst : OrderBot α] {a : α} :

BoundedOrder ↑(Set.Iic a)

Equations

Set.Iic.instBoundedOrderElemIicLeToLEMemSetInstMembershipSet = let src := Set.Iic.orderTop; let src_1 := Set.Iic.orderBot; BoundedOrder.mk

instance Set.Ici.semilatticeInf {α : Type u_1} [inst : SemilatticeInf α] {a : α} :

SemilatticeInf ↑(Set.Ici a)

Equations

Set.Ici.semilatticeInf = Subtype.semilatticeInf (_ : ∀ (x x_1 : α), x ∈ Set.Ici a → x_1 ∈ Set.Ici a → a ≤ x ⊓ x_1)

instance Set.Ici.semilatticeSup {α : Type u_1} [inst : SemilatticeSup α] {a : α} :

SemilatticeSup ↑(Set.Ici a)

Equations

Set.Ici.semilatticeSup = Subtype.semilatticeSup (_ : ∀ (x x_1 : α), x ∈ Set.Ici a → x_1 ∈ Set.Ici a → a ≤ x ⊔ x_1)

instance Set.Ici.lattice {α : Type u_1} [inst : Lattice α] {a : α} :

Lattice ↑(Set.Ici a)

Equations

One or more equations did not get rendered due to their size.

instance Set.Ici.distribLattice {α : Type u_1} [inst : DistribLattice α] {a : α} :

DistribLattice ↑(Set.Ici a)

Equations

Set.Ici.distribLattice = let src := Set.Ici.lattice; DistribLattice.mk (_ : ∀ (x x_1 x_2 : ↑(Set.Ici a)), (↑x ⊔ ↑x_1) ⊓ (↑x ⊔ ↑x_2) ≤ ↑x ⊔ ↑x_1 ⊓ ↑x_2)

instance Set.Ici.orderBot {α : Type u_1} [inst : Preorder α] {a : α} :

OrderBot ↑(Set.Ici a)

Equations

Set.Ici.orderBot = OrderBot.mk (_ : ∀ (x : ↑(Set.Ici a)), ↑x ∈ Set.Ici a)

@[simp]

theorem Set.Ici.coe_bot {α : Type u_1} [inst : Preorder α] {a : α} :

↑⊥ = a

instance Set.Ici.orderTop {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {a : α} :

OrderTop ↑(Set.Ici a)

Equations

Set.Ici.orderTop = OrderTop.mk (_ : ∀ (x : ↑(Set.Ici a)), x ≤ ⊤)

@[simp]

theorem Set.Ici.coe_top {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {a : α} :

instance Set.Ici.boundedOrder {α : Type u_1} [inst : Preorder α] [inst : OrderTop α] {a : α} :

BoundedOrder ↑(Set.Ici a)

Equations

Set.Ici.boundedOrder = let src := Set.Ici.orderTop; let src_1 := Set.Ici.orderBot; BoundedOrder.mk

instance Set.Icc.semilatticeInf {α : Type u_1} [inst : SemilatticeInf α] {a : α} {b : α} :

SemilatticeInf ↑(Set.Icc a b)

Equations

Set.Icc.semilatticeInf = Subtype.semilatticeInf (_ : ∀ (x x_1 : α), x ∈ Set.Icc a b → x_1 ∈ Set.Icc a b → a ≤ x ⊓ x_1 ∧ x ⊓ x_1 ≤ b)

instance Set.Icc.semilatticeSup {α : Type u_1} [inst : SemilatticeSup α] {a : α} {b : α} :

SemilatticeSup ↑(Set.Icc a b)

Equations

Set.Icc.semilatticeSup = Subtype.semilatticeSup (_ : ∀ (x x_1 : α), x ∈ Set.Icc a b → x_1 ∈ Set.Icc a b → a ≤ x ⊔ x_1 ∧ x ⊔ x_1 ≤ b)

instance Set.Icc.lattice {α : Type u_1} [inst : Lattice α] {a : α} {b : α} :

Lattice ↑(Set.Icc a b)

Equations

One or more equations did not get rendered due to their size.

def Set.Icc.orderBot {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (h : a ≤ b) :

OrderBot ↑(Set.Icc a b)

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

Equations

Set.Icc.orderBot h = IsLeast.orderBot (_ : IsLeast (Set.Icc a b) a)

def Set.Icc.orderTop {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (h : a ≤ b) :

OrderTop ↑(Set.Icc a b)

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

Equations

Set.Icc.orderTop h = IsGreatest.orderTop (_ : IsGreatest (Set.Icc a b) b)

def Set.Icc.boundedOrder {α : Type u_1} [inst : Preorder α] {a : α} {b : α} (h : a ≤ b) :

BoundedOrder ↑(Set.Icc a b)

Icc a b is a bounded_order whenever a ≤ b≤ b.

Equations

Set.Icc.boundedOrder h = let src := Set.Icc.orderTop h; let src_1 := Set.Icc.orderBot h; BoundedOrder.mk