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 β.

source
instance Sum.Lex.instSemilatticeSup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] :
SemilatticeSup (Lex (α ⊕ β))
Equations
source
@[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₂
source
@[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₂
source
instance Sum.Lex.instSemilatticeInf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] :
SemilatticeInf (Lex (α ⊕ β))
Equations
source
@[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₂
source
@[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₂
source
instance Sum.Lex.instLattice {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] :
Lattice (Lex (α ⊕ β))
Equations
  • Sum.Lex.instLattice = let __src := Sum.Lex.instSemilatticeSup; let __src_1 := Sum.Lex.instSemilatticeInf; Lattice.mk ⋯ ⋯ ⋯
source
def Sum.Lex.inlLatticeHom {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] :
LatticeHom α (Lex (α ⊕ β))

Sum.Lex.inlₗ as a lattice homomorphism.

Equations
  • Sum.Lex.inlLatticeHom = { toFun := Sum.inlₗ, map_sup' := ⋯, map_inf' := ⋯ }
Instances For
    source
    def Sum.Lex.inrLatticeHom {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] :
    LatticeHom β (Lex (α ⊕ β))

    Sum.Lex.inrₗ as a lattice homomorphism.

    Equations
    • Sum.Lex.inrLatticeHom = { toFun := Sum.inrₗ, map_sup' := ⋯, map_inf' := ⋯ }
    Instances For
      source
      instance Sum.Lex.instDistribLattice {α : Type u_1} {β : Type u_2} [DistribLattice α] [DistribLattice β] :
      DistribLattice (Lex (α ⊕ β))
      Equations