# Documentation

Mathlib.Data.Sum.Lattice

# 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} [] [] :
Equations
@[simp]
theorem Sum.Lex.inl_sup {α : Type u_1} {β : Type u_2} [] [] (a₁ : α) (a₂ : α) :
Sum.inlₗ (a₁ a₂) = Sum.inlₗ a₁ Sum.inlₗ a₂
@[simp]
theorem Sum.Lex.inr_sup {α : Type u_1} {β : Type u_2} [] [] (b₁ : β) (b₂ : β) :
Sum.inrₗ (b₁ b₂) = Sum.inrₗ b₁ Sum.inrₗ b₂
instance Sum.Lex.instSemilatticeInf {α : Type u_1} {β : Type u_2} [] [] :
Equations
@[simp]
theorem Sum.Lex.inl_inf {α : Type u_1} {β : Type u_2} [] [] (a₁ : α) (a₂ : α) :
Sum.inlₗ (a₁ a₂) = Sum.inlₗ a₁ Sum.inlₗ a₂
@[simp]
theorem Sum.Lex.inr_inf {α : Type u_1} {β : Type u_2} [] [] (b₁ : β) (b₂ : β) :
Sum.inrₗ (b₁ b₂) = Sum.inrₗ b₁ Sum.inrₗ b₂
instance Sum.Lex.instLattice {α : Type u_1} {β : Type u_2} [] [] :
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} [] [] :
LatticeHom α (Lex (α β))

Sum.Lex.inlₗ as a lattice homomorphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Sum.Lex.inrLatticeHom {α : Type u_1} {β : Type u_2} [] [] :
LatticeHom β (Lex (α β))

Sum.Lex.inrₗ as a lattice homomorphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance Sum.Lex.instDistribLattice {α : Type u_1} {β : Type u_2} [] [] :
Equations