Documentation

Mathlib.Order.Hom.Order

Lattice structure on order homomorphisms #

This file defines the lattice structure on order homomorphisms, which are bundled monotone functions.

Main definitions #

Tags #

monotone map, bundled morphism

source
instance OrderHom.instMax {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeSup β] :
Max (α →o β)
Equations
    source
    @[simp]
    theorem OrderHom.coe_sup {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeSup β] (f g : α →o β) :
    ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
    source
    instance OrderHom.instSemilatticeSup {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeSup β] :
    SemilatticeSup (α →o β)
    Equations
      source
      instance OrderHom.instMin {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeInf β] :
      Min (α →o β)
      Equations
        source
        @[simp]
        theorem OrderHom.coe_inf {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeInf β] (f g : α →o β) :
        ⇑(f ⊓ g) = ⇑f ⊓ ⇑g
        source
        instance OrderHom.instSemilatticeInf {α : Type u_1} {β : Type u_2} [Preorder α] [SemilatticeInf β] :
        SemilatticeInf (α →o β)
        Equations
          source
          instance OrderHom.lattice {α : Type u_1} {β : Type u_2} [Preorder α] [Lattice β] :
          Lattice (α →o β)
          Equations
            source
            instance OrderHom.instBotOfOrderBot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] :
            Bot (α →o β)
            Equations
              source
              @[simp]
              theorem OrderHom.bot_def {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] :
              ⊥ = (const α) ⊥
              source
              instance OrderHom.orderBot {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderBot β] :
              OrderBot (α →o β)
              Equations
                source
                instance OrderHom.instTopOrderHom {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] :
                Top (α →o β)
                Equations
                  source
                  @[simp]
                  theorem OrderHom.top_def {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] :
                  ⊤ = (const α) ⊤
                  source
                  instance OrderHom.orderTop {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [OrderTop β] :
                  OrderTop (α →o β)
                  Equations
                    source
                    instance OrderHom.instInfSet {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] :
                    InfSet (α →o β)
                    Equations
                      source
                      @[simp]
                      theorem OrderHom.sInf_apply {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] (s : Set (α →o β)) (x : α) :
                      (sInf s) x = ⨅ f ∈ s, f x
                      source
                      theorem OrderHom.iInf_apply {α : Type u_1} {β : Type u_2} [Preorder α] {ι : Sort u_3} [CompleteLattice β] (f : ι → α →o β) (x : α) :
                      (⨅ (i : ι), f i) x = ⨅ (i : ι), (f i) x
                      source
                      @[simp]
                      theorem OrderHom.coe_iInf {α : Type u_1} {β : Type u_2} [Preorder α] {ι : Sort u_3} [CompleteLattice β] (f : ι → α →o β) :
                      ⇑(⨅ (i : ι), f i) = ⨅ (i : ι), ⇑(f i)
                      source
                      instance OrderHom.instSupSet {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] :
                      SupSet (α →o β)
                      Equations
                        source
                        @[simp]
                        theorem OrderHom.sSup_apply {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] (s : Set (α →o β)) (x : α) :
                        (sSup s) x = ⨆ f ∈ s, f x
                        source
                        theorem OrderHom.iSup_apply {α : Type u_1} {β : Type u_2} [Preorder α] {ι : Sort u_3} [CompleteLattice β] (f : ι → α →o β) (x : α) :
                        (⨆ (i : ι), f i) x = ⨆ (i : ι), (f i) x
                        source
                        @[simp]
                        theorem OrderHom.coe_iSup {α : Type u_1} {β : Type u_2} [Preorder α] {ι : Sort u_3} [CompleteLattice β] (f : ι → α →o β) :
                        ⇑(⨆ (i : ι), f i) = ⨆ (i : ι), ⇑(f i)
                        source
                        instance OrderHom.instCompleteLattice {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] :
                        CompleteLattice (α →o β)
                        Equations
                          source
                          theorem OrderHom.iterate_sup_le_sup_iff {α : Type u_3} [SemilatticeSup α] (f : α →o α) :
                          (∀ (n₁ n₂ : ℕ) (a₁ a₂ : α), (⇑f)^[n₁ + n₂] (a₁ ⊔ a₂) ≤ (⇑f)^[n₁] a₁ ⊔ (⇑f)^[n₂] a₂) ↔ ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂