# 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*.semilatticeInf`
- `Set.I*c.orderTop`
- `Set.I*c.semilatticeInf`
- `Set.I**.lattice`
- `Set.Iic.boundedOrder`, within an `OrderBot`
- `Set.Ici.boundedOrder`, within an `OrderTop`

source
instance Set.Ico.semilatticeInf {α : Type u_1} [SemilatticeInf α] {a b : α} :
SemilatticeInf ↑(Ico a b)
Equations

- Set.Ico.semilatticeInf = Subtype.semilatticeInf ⋯

source
@[simp]
theorem Set.Ico.coe_inf {α : Type u_1} [SemilatticeInf α] {a b : α} {x y : ↑(Ico a b)} :
↑(x ⊓ y) = ↑x ⊓ ↑y
source
instance Set.Ico.orderBot {α : Type u_1} [PartialOrder α] {a b : α} [Fact (a < b)] :
OrderBot ↑(Ico a b)

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

Equations

- Set.Ico.orderBot = ⋯.orderBot

source
@[simp]
theorem Set.Ico.coe_bot {α : Type u_1} [PartialOrder α] (a b : α) [Fact (a < b)] :
↑⊥ = a
source
theorem Set.Ico.disjoint_iff {α : Type u_1} [SemilatticeInf α] {a b : α} [Fact (a < b)] {x y : ↑(Ico a b)} :
Disjoint x y ↔ ↑x ⊓ ↑y = a
source
instance Set.Iio.semilatticeInf {α : Type u_1} [SemilatticeInf α] {a : α} :
SemilatticeInf ↑(Iio a)
Equations

- Set.Iio.semilatticeInf = Subtype.semilatticeInf ⋯

source
@[simp]
theorem Set.Iio.coe_inf {α : Type u_1} [SemilatticeInf α] {a : α} {x y : ↑(Iio a)} :
↑(x ⊓ y) = ↑x ⊓ ↑y
source
instance Set.Ioc.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a b : α} :
SemilatticeSup ↑(Ioc a b)
Equations

- Set.Ioc.semilatticeSup = Subtype.semilatticeSup ⋯

source
@[simp]
theorem Set.Ioc.coe_sup {α : Type u_1} [SemilatticeSup α] {a b : α} {x y : ↑(Ioc a b)} :
↑(x ⊔ y) = ↑x ⊔ ↑y
source
instance Set.Ioc.orderTop {α : Type u_1} [PartialOrder α] {a b : α} [Fact (a < b)] :
OrderTop ↑(Ioc a b)

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

Equations

- Set.Ioc.orderTop = ⋯.orderTop

source
@[simp]
theorem Set.Ioc.coe_top {α : Type u_1} [PartialOrder α] (a b : α) [Fact (a < b)] :
↑⊤ = b
source
theorem Set.Ioc.codisjoint_iff {α : Type u_1} [SemilatticeSup α] {a b : α} [Fact (a < b)] {x y : ↑(Ioc a b)} :
Codisjoint x y ↔ ↑x ⊔ ↑y = b
source
instance Set.Ioi.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} :
SemilatticeSup ↑(Ioi a)
Equations

- Set.Ioi.semilatticeSup = Subtype.semilatticeSup ⋯

source
@[simp]
theorem Set.Ioi.coe_sup {α : Type u_1} [SemilatticeSup α] {a : α} {x y : ↑(Ioi a)} :
↑(x ⊔ y) = ↑x ⊔ ↑y
source
instance Set.Iic.semilatticeInf {α : Type u_1} {a : α} [SemilatticeInf α] :
SemilatticeInf ↑(Iic a)
Equations

- Set.Iic.semilatticeInf = Subtype.semilatticeInf ⋯

source
@[simp]
theorem Set.Iic.coe_inf {α : Type u_1} {a : α} [SemilatticeInf α] {x y : ↑(Iic a)} :
↑(x ⊓ y) = ↑x ⊓ ↑y
source
instance Set.Iic.semilatticeSup {α : Type u_1} {a : α} [SemilatticeSup α] :
SemilatticeSup ↑(Iic a)
Equations

- Set.Iic.semilatticeSup = Subtype.semilatticeSup ⋯

source
@[simp]
theorem Set.Iic.coe_sup {α : Type u_1} {a : α} [SemilatticeSup α] {x y : ↑(Iic a)} :
↑(x ⊔ y) = ↑x ⊔ ↑y
source
instance Set.Iic.instLatticeElem {α : Type u_1} {a : α} [Lattice α] :
Lattice ↑(Iic a)
Equations

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

source
instance Set.Iic.orderTop {α : Type u_1} {a : α} [Preorder α] :
OrderTop ↑(Iic a)
Equations

- Set.Iic.orderTop = { top := ⟨a, ⋯⟩, le_top := ⋯ }

source
@[simp]
theorem Set.Iic.coe_top {α : Type u_1} [Preorder α] (a : α) :
↑⊤ = a
source
theorem Set.Iic.eq_top_iff {α : Type u_1} {a : α} [Preorder α] {x : ↑(Iic a)} :
x = ⊤ ↔ ↑x = a
source
instance Set.Iic.orderBot {α : Type u_1} {a : α} [Preorder α] [OrderBot α] :
OrderBot ↑(Iic a)
Equations

- Set.Iic.orderBot = { bot := ⟨⊥, ⋯⟩, bot_le := ⋯ }

source
@[simp]
theorem Set.Iic.coe_bot {α : Type u_1} [Preorder α] [OrderBot α] (a : α) :
↑⊥ = ⊥
source
instance Set.Iic.instBoundedOrderElemOfOrderBot {α : Type u_1} {a : α} [Preorder α] [OrderBot α] :
BoundedOrder ↑(Iic a)
Equations

- Set.Iic.instBoundedOrderElemOfOrderBot = { toOrderTop := Set.Iic.orderTop, toOrderBot := Set.Iic.orderBot }

source
theorem Set.Iic.disjoint_iff {α : Type u_1} {a : α} [SemilatticeInf α] [OrderBot α] {x y : ↑(Iic a)} :
Disjoint x y ↔ Disjoint ↑x ↑y
source
theorem Set.Iic.codisjoint_iff {α : Type u_1} {a : α} [SemilatticeSup α] {x y : ↑(Iic a)} :
Codisjoint x y ↔ ↑x ⊔ ↑y = a
source
theorem Set.Iic.isCompl_iff {α : Type u_1} {a : α} [Lattice α] [OrderBot α] {x y : ↑(Iic a)} :
IsCompl x y ↔ Disjoint ↑x ↑y ∧ ↑x ⊔ ↑y = a
source
theorem Set.Iic.complementedLattice_iff {α : Type u_1} {a : α} [Lattice α] [OrderBot α] :
ComplementedLattice ↑(Iic a) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
source
instance Set.Ici.semilatticeInf {α : Type u_1} [SemilatticeInf α] {a : α} :
SemilatticeInf ↑(Ici a)
Equations

- Set.Ici.semilatticeInf = Subtype.semilatticeInf ⋯

source
@[simp]
theorem Set.Ici.coe_inf {α : Type u_1} [SemilatticeInf α] {a : α} {x y : ↑(Ici a)} :
↑(x ⊓ y) = ↑x ⊓ ↑y
source
instance Set.Ici.semilatticeSup {α : Type u_1} [SemilatticeSup α] {a : α} :
SemilatticeSup ↑(Ici a)
Equations

- Set.Ici.semilatticeSup = Subtype.semilatticeSup ⋯

source
@[simp]
theorem Set.Ici.coe_sup {α : Type u_1} [SemilatticeSup α] {a : α} {x y : ↑(Ici a)} :
↑(x ⊔ y) = ↑x ⊔ ↑y
source
instance Set.Ici.lattice {α : Type u_1} [Lattice α] {a : α} :
Lattice ↑(Ici a)
Equations

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

source
instance Set.Ici.distribLattice {α : Type u_1} [DistribLattice α] {a : α} :
DistribLattice ↑(Ici a)
Equations

- Set.Ici.distribLattice = { toLattice := Set.Ici.lattice, le_sup_inf := ⋯ }

source
instance Set.Ici.orderBot {α : Type u_1} [Preorder α] {a : α} :
OrderBot ↑(Ici a)
Equations

- Set.Ici.orderBot = { bot := ⟨a, ⋯⟩, bot_le := ⋯ }

source
@[simp]
theorem Set.Ici.coe_bot {α : Type u_1} [Preorder α] (a : α) :
↑⊥ = a
source
instance Set.Ici.orderTop {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
OrderTop ↑(Ici a)
Equations

- Set.Ici.orderTop = { top := ⟨⊤, ⋯⟩, le_top := ⋯ }

source
@[simp]
theorem Set.Ici.coe_top {α : Type u_1} [Preorder α] [OrderTop α] (a : α) :
↑⊤ = ⊤
source
instance Set.Ici.boundedOrder {α : Type u_1} [Preorder α] [OrderTop α] {a : α} :
BoundedOrder ↑(Ici a)
Equations

- Set.Ici.boundedOrder = { toOrderTop := Set.Ici.orderTop, toOrderBot := Set.Ici.orderBot }

source
theorem Set.Ici.disjoint_iff {α : Type u_1} [SemilatticeInf α] {a : α} {x y : ↑(Ici a)} :
Disjoint x y ↔ ↑x ⊓ ↑y = a
source
theorem Set.Ici.codisjoint_iff {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {x y : ↑(Ici a)} :
Codisjoint x y ↔ Codisjoint ↑x ↑y
source
theorem Set.Ici.isCompl_iff {α : Type u_1} [Lattice α] [OrderTop α] {a : α} {x y : ↑(Ici a)} :
IsCompl x y ↔ ↑x ⊓ ↑y = a ∧ Codisjoint ↑x ↑y
source
instance Set.Icc.semilatticeInf {α : Type u_1} {a b : α} [SemilatticeInf α] :
SemilatticeInf ↑(Icc a b)
Equations

- Set.Icc.semilatticeInf = Subtype.semilatticeInf ⋯

source
@[simp]
theorem Set.Icc.coe_inf {α : Type u_1} {a b : α} [SemilatticeInf α] {x y : ↑(Icc a b)} :
↑(x ⊓ y) = ↑x ⊓ ↑y
source
instance Set.Icc.semilatticeSup {α : Type u_1} {a b : α} [SemilatticeSup α] :
SemilatticeSup ↑(Icc a b)
Equations

- Set.Icc.semilatticeSup = Subtype.semilatticeSup ⋯

source
@[simp]
theorem Set.Icc.coe_sup {α : Type u_1} {a b : α} [SemilatticeSup α] {x y : ↑(Icc a b)} :
↑(x ⊔ y) = ↑x ⊔ ↑y
source
instance Set.Icc.lattice {α : Type u_1} {a b : α} [Lattice α] :
Lattice ↑(Icc a b)
Equations

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

source
instance Set.Icc.instOrderBotElemOfFactLe {α : Type u_1} {a b : α} [Preorder α] [Fact (a ≤ b)] :
OrderBot ↑(Icc a b)

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

Equations

- Set.Icc.instOrderBotElemOfFactLe = ⋯.orderBot

source
@[simp]
theorem Set.Icc.coe_bot {α : Type u_1} [Preorder α] (a b : α) [Fact (a ≤ b)] :
↑⊥ = a
source
instance Set.Icc.instOrderTopElemOfFactLe {α : Type u_1} {a b : α} [Preorder α] [Fact (a ≤ b)] :
OrderTop ↑(Icc a b)

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

Equations

- Set.Icc.instOrderTopElemOfFactLe = ⋯.orderTop

source
@[simp]
theorem Set.Icc.coe_top {α : Type u_1} [Preorder α] (a b : α) [Fact (a ≤ b)] :
↑⊤ = b
source
instance Set.Icc.instBoundedOrderElemOfFactLe {α : Type u_1} {a b : α} [Preorder α] [Fact (a ≤ b)] :
BoundedOrder ↑(Icc a b)

`Icc a b` is a `BoundedOrder` whenever `a ≤ b`.

Equations

- Set.Icc.instBoundedOrderElemOfFactLe = { toOrderTop := Set.Icc.instOrderTopElemOfFactLe, toOrderBot := Set.Icc.instOrderBotElemOfFactLe }

source
theorem Set.Icc.disjoint_iff {α : Type u_1} {a b : α} [SemilatticeInf α] [Fact (a ≤ b)] {x y : ↑(Icc a b)} :
Disjoint x y ↔ ↑x ⊓ ↑y = a
source
theorem Set.Icc.codisjoint_iff {α : Type u_1} {a b : α} [SemilatticeSup α] [Fact (a ≤ b)] {x y : ↑(Icc a b)} :
Codisjoint x y ↔ ↑x ⊔ ↑y = b
source
theorem Set.Icc.isCompl_iff {α : Type u_1} {a b : α} [Lattice α] [Fact (a ≤ b)] {x y : ↑(Icc a b)} :
IsCompl x y ↔ ↑x ⊓ ↑y = a ∧ ↑x ⊔ ↑y = b