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_reducible]

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

Equations

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

@[simp]

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

@[simp]

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

@[instance_reducible]

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

Equations

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

@[simp]

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

@[simp]

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

@[instance_reducible]

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

Equations

• Sum.Lex.instLattice = { toSemilatticeSup := Sum.Lex.instSemilatticeSup, inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

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

Sum.Lex.inlₗ as a lattice homomorphism.

Equations

• Sum.Lex.inlLatticeHom = { toFun := Sum.inlₗ, map_sup' := ⋯, map_inf' := ⋯ }

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

Sum.Lex.inrₗ as a lattice homomorphism.

Equations

• Sum.Lex.inrLatticeHom = { toFun := Sum.inrₗ, map_sup' := ⋯, map_inf' := ⋯ }

@[instance_reducible]

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

Equations

• Sum.Lex.instDistribLattice = { toLattice := Sum.Lex.instLattice, le_sup_inf := ⋯ }