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 (_root_.Lex (α ⊕ β))
Equations
    source
    @[simp]
    theorem Sum.Lex.inl_sup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (a₁ a₂ : α) :
    inlₗ (a₁ ⊔ a₂) = inlₗ a₁ ⊔ inlₗ a₂
    source
    @[simp]
    theorem Sum.Lex.inr_sup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (b₁ b₂ : β) :
    inrₗ (b₁ ⊔ b₂) = inrₗ b₁ ⊔ inrₗ b₂
    source
    instance Sum.Lex.instSemilatticeInf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] :
    SemilatticeInf (_root_.Lex (α ⊕ β))
    Equations
      source
      @[simp]
      theorem Sum.Lex.inl_inf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (a₁ a₂ : α) :
      inlₗ (a₁ ⊓ a₂) = inlₗ a₁ ⊓ inlₗ a₂
      source
      @[simp]
      theorem Sum.Lex.inr_inf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (b₁ b₂ : β) :
      inrₗ (b₁ ⊓ b₂) = inrₗ b₁ ⊓ inrₗ b₂
      source
      instance Sum.Lex.instLattice {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] :
      Lattice (_root_.Lex (α ⊕ β))
      Equations
        source
        def Sum.Lex.inlLatticeHom {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] :
        LatticeHom α (_root_.Lex (α ⊕ β))

        Sum.Lex.inlₗ as a lattice homomorphism.

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

            Sum.Lex.inrₗ as a lattice homomorphism.

            Equations
              Instances For
                source
                instance Sum.Lex.instDistribLattice {α : Type u_1} {β : Type u_2} [DistribLattice α] [DistribLattice β] :
                DistribLattice (_root_.Lex (α ⊕ β))
                Equations