Lexicographic sum of lattices

This file proves that we can combine two lattices α and β into a lattice α ⊕ₗ β where everything in α is declared smaller than everything in β.

instance Sum.Lex.instSemilatticeSup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] : SemilatticeSup (Lex (α ⊕ β))

Equations

• Sum.Lex.instSemilatticeSup = SemilatticeSup.mk (_ : ∀ (x y : Lex (α ⊕ β)), x ≤ x ⊔ y) (_ : ∀ (x y : Lex (α ⊕ β)), y ≤ x ⊔ y) (_ : ∀ (x y z : Lex (α ⊕ β)), x ≤ z → y ≤ z → x ⊔ y ≤ z)

@[simp]

theorem Sum.Lex.inl_sup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (a₁ : α) (a₂ : α) : Sum.inlₗ (a₁ ⊔ a₂) = Sum.inlₗ a₁ ⊔ Sum.inlₗ a₂

@[simp]

theorem Sum.Lex.inr_sup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (b₁ : β) (b₂ : β) : Sum.inrₗ (b₁ ⊔ b₂) = Sum.inrₗ b₁ ⊔ Sum.inrₗ b₂

instance Sum.Lex.instSemilatticeInf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] : SemilatticeInf (Lex (α ⊕ β))

Equations

• Sum.Lex.instSemilatticeInf = SemilatticeInf.mk (_ : ∀ (x y : Lex (α ⊕ β)), x ⊓ y ≤ x) (_ : ∀ (x y : Lex (α ⊕ β)), x ⊓ y ≤ y) (_ : ∀ (x y z : Lex (α ⊕ β)), x ≤ y → x ≤ z → x ≤ y ⊓ z)

@[simp]

theorem Sum.Lex.inl_inf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (a₁ : α) (a₂ : α) : Sum.inlₗ (a₁ ⊓ a₂) = Sum.inlₗ a₁ ⊓ Sum.inlₗ a₂

@[simp]

theorem Sum.Lex.inr_inf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (b₁ : β) (b₂ : β) : Sum.inrₗ (b₁ ⊓ b₂) = Sum.inrₗ b₁ ⊓ Sum.inrₗ b₂

instance Sum.Lex.instLattice {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] : Lattice (Lex (α ⊕ β))

Equations

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

def Sum.Lex.inlLatticeHom {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] : LatticeHom α (Lex (α ⊕ β))

Sum.Lex.inlₗ as a lattice homomorphism.

Equations

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

def Sum.Lex.inrLatticeHom {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] : LatticeHom β (Lex (α ⊕ β))

Sum.Lex.inrₗ as a lattice homomorphism.

Equations

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

instance Sum.Lex.instDistribLattice {α : Type u_1} {β : Type u_2} [DistribLattice α] [DistribLattice β] : DistribLattice (Lex (α ⊕ β))

Equations

• Sum.Lex.instDistribLattice = DistribLattice.mk (_ : ∀ (a a_1 : Lex (α ⊕ β)) (a_2 : Lex (α ⊕ β)), (a ⊔ a_1) ⊓ (a ⊔ a_2) ≤ a ⊔ a_1 ⊓ a_2)