Adjoining ⊤ and ⊥ to order maps and lattice homomorphisms

This file defines ways to adjoin ⊤ or ⊥ or both to order maps (homomorphisms, embeddings and isomorphisms) and lattice homomorphisms, and properties about the results.

Some definitions cause a possibly unbounded lattice homomorphism to become bounded, so they change the type of the homomorphism.

def WithTop.toDualBotEquiv {α : Type u_1} [LE α] : WithTop αᵒᵈ ≃o (WithBot α)ᵒᵈ

Taking the dual then adding ⊤ is the same as adding ⊥ then taking the dual. This is the order iso form of WithTop.ofDual, as proven by coe_toDualBotEquiv.

@[simp]

theorem WithTop.toDualBotEquiv_coe {α : Type u_1} [LE α] (a : α) : WithTop.toDualBotEquiv ↑(OrderDual.toDual a) = OrderDual.toDual ↑a

@[simp]

theorem WithTop.toDualBotEquiv_symm_coe {α : Type u_1} [LE α] (a : α) : WithTop.toDualBotEquiv.symm (OrderDual.toDual ↑a) = ↑(OrderDual.toDual a)

@[simp]

theorem WithTop.toDualBotEquiv_top {α : Type u_1} [LE α] : WithTop.toDualBotEquiv ⊤ = ⊤

@[simp]

theorem WithTop.toDualBotEquiv_symm_top {α : Type u_1} [LE α] : WithTop.toDualBotEquiv.symm ⊤ = ⊤

theorem WithTop.coe_toDualBotEquiv {α : Type u_1} [LE α] : ⇑WithTop.toDualBotEquiv = ⇑OrderDual.toDual ∘ ⇑WithTop.ofDual

def Function.Embedding.coeWithTop {α : Type u_1} : α ↪ WithTop α

Embedding into WithTop α.

@[simp]

theorem Function.Embedding.coeWithTop_apply {α : Type u_1} (a✝ : α) : coeWithTop a✝ = ↑a✝

def WithTop.coeOrderHom {α : Type u_4} [Preorder α] : α ↪o WithTop α

The coercion α → WithTop α bundled as monotone map.

@[simp]

theorem WithTop.coeOrderHom_apply {α : Type u_4} [Preorder α] : ⇑coeOrderHom = some

def WithTop.subtypeOrderIso {α : Type u_1} [PartialOrder α] [OrderTop α] [DecidablePred fun (x : α) => x = ⊤] : WithTop { a : α // a ≠ ⊤ } ≃o α

Any OrderTop is equivalent to WithTop of the subtype excluding ⊤.

See also Equiv.optionSubtypeNe.

@[simp]

theorem WithTop.subtypeOrderIso_apply_coe {α : Type u_1} [PartialOrder α] [OrderTop α] [DecidablePred fun (x : α) => x = ⊤] (a : { a : α // a ≠ ⊤ }) : subtypeOrderIso ↑a = ↑a

theorem WithTop.subtypeOrderIso_symm_apply {α : Type u_1} [PartialOrder α] [OrderTop α] [DecidablePred fun (x : α) => x = ⊤] {a : α} (h : a ≠ ⊤) : subtypeOrderIso.symm a = ↑⟨a, h⟩

def WithBot.toDualTopEquiv {α : Type u_1} [LE α] : WithBot αᵒᵈ ≃o (WithTop α)ᵒᵈ

Taking the dual then adding ⊥ is the same as adding ⊤ then taking the dual. This is the order iso form of WithBot.ofDual, as proven by coe_toDualTopEquiv.

@[simp]

theorem WithBot.toDualTopEquiv_coe {α : Type u_1} [LE α] (a : α) : WithBot.toDualTopEquiv ↑(OrderDual.toDual a) = OrderDual.toDual ↑a

@[simp]

theorem WithBot.toDualTopEquiv_symm_coe {α : Type u_1} [LE α] (a : α) : WithBot.toDualTopEquiv.symm (OrderDual.toDual ↑a) = ↑(OrderDual.toDual a)

@[simp]

theorem WithBot.toDualTopEquiv_bot {α : Type u_1} [LE α] : WithBot.toDualTopEquiv ⊥ = ⊥

@[simp]

theorem WithBot.toDualTopEquiv_symm_bot {α : Type u_1} [LE α] : WithBot.toDualTopEquiv.symm ⊥ = ⊥

theorem WithBot.coe_toDualTopEquiv_eq {α : Type u_1} [LE α] : ⇑WithBot.toDualTopEquiv = ⇑OrderDual.toDual ∘ ⇑WithBot.ofDual

def Function.Embedding.coeWithBot {α : Type u_1} : α ↪ WithBot α

Embedding into WithBot α.

@[simp]

theorem Function.Embedding.coeWithBot_apply {α : Type u_1} (a✝ : α) : coeWithBot a✝ = ↑a✝

def WithBot.coeOrderHom {α : Type u_4} [Preorder α] : α ↪o WithBot α

The coercion α → WithBot α bundled as monotone map.

@[simp]

theorem WithBot.coeOrderHom_apply {α : Type u_4} [Preorder α] : ⇑coeOrderHom = some

def WithBot.subtypeOrderIso {α : Type u_1} [PartialOrder α] [OrderBot α] [DecidablePred fun (x : α) => x = ⊥] : WithBot { a : α // a ≠ ⊥ } ≃o α

Any OrderBot is equivalent to WithBot of the subtype excluding ⊥.

See also Equiv.optionSubtypeNe.

@[simp]

theorem WithBot.subtypeOrderIso_apply_coe {α : Type u_1} [PartialOrder α] [OrderBot α] [DecidablePred fun (x : α) => x = ⊥] (a : { a : α // a ≠ ⊥ }) : subtypeOrderIso ↑a = ↑a

theorem WithBot.subtypeOrderIso_symm_apply {α : Type u_1} [PartialOrder α] [OrderBot α] [DecidablePred fun (x : α) => x = ⊥] {a : α} (h : a ≠ ⊥) : subtypeOrderIso.symm a = ↑⟨a, h⟩

def OrderHom.withBotMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) : WithBot α →o WithBot β

Lift an order homomorphism f : α →o β to an order homomorphism WithBot α →o WithBot β.

@[simp]

theorem OrderHom.withBotMap_coe {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) : ⇑f.withBotMap = WithBot.map ⇑f

def OrderHom.withTopMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) : WithTop α →o WithTop β

Lift an order homomorphism f : α →o β to an order homomorphism WithTop α →o WithTop β.

@[simp]

theorem OrderHom.withTopMap_coe {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α →o β) : ⇑f.withTopMap = WithTop.map ⇑f

def OrderEmbedding.withBotMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) : WithBot α ↪o WithBot β

A version of WithBot.map for order embeddings.

@[simp]

theorem OrderEmbedding.withBotMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) : ⇑f.withBotMap = WithBot.map ⇑f

def OrderEmbedding.withTopMap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) : WithTop α ↪o WithTop β

A version of WithTop.map for order embeddings.

@[simp]

theorem OrderEmbedding.withTopMap_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) : ⇑f.withTopMap = WithTop.map ⇑f

def OrderIso.withTopCongr {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : WithTop α ≃o WithTop β

A version of Equiv.optionCongr for WithTop.

@[simp]

theorem OrderIso.withTopCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : ⇑e.withTopCongr = WithTop.map ⇑e

@[simp]

theorem OrderIso.withTopCongr_symm_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : ⇑(RelIso.symm e.withTopCongr) = e.withTopCongr.invFun

@[simp]

theorem OrderIso.withTopCongr_refl {α : Type u_1} [PartialOrder α] : (refl α).withTopCongr = refl (WithTop α)

@[simp]

theorem OrderIso.withTopCongr_symm {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : e.symm.withTopCongr = e.withTopCongr.symm

@[simp]

theorem OrderIso.withTopCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PartialOrder α] [PartialOrder β] [PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) : (e₁.trans e₂).withTopCongr = e₁.withTopCongr.trans e₂.withTopCongr

def OrderIso.withBotCongr {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : WithBot α ≃o WithBot β

A version of Equiv.optionCongr for WithBot.

@[simp]

theorem OrderIso.withBotCongr_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : ⇑e.withBotCongr = WithBot.map ⇑e

@[simp]

theorem OrderIso.withBotCongr_symm_apply {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : ⇑(RelIso.symm e.withBotCongr) = e.withBotCongr.invFun

@[simp]

theorem OrderIso.withBotCongr_refl {α : Type u_1} [PartialOrder α] : (refl α).withBotCongr = refl (WithBot α)

@[simp]

theorem OrderIso.withBotCongr_symm {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (e : α ≃o β) : e.symm.withBotCongr = e.withBotCongr.symm

@[simp]

theorem OrderIso.withBotCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PartialOrder α] [PartialOrder β] [PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) : (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

def SupHom.withTop {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) : SupHom (WithTop α) (WithTop β)

Adjoins a ⊤ to the domain and codomain of a SupHom.

@[simp]

theorem SupHom.withTop_toFun {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) (a✝ : WithTop α) : f.withTop a✝ = WithTop.map (⇑f) a✝

@[simp]

theorem SupHom.withTop_id {α : Type u_1} [SemilatticeSup α] : (SupHom.id α).withTop = SupHom.id (WithTop α)

@[simp]

theorem SupHom.withTop_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [SemilatticeSup β] [SemilatticeSup γ] (f : SupHom β γ) (g : SupHom α β) : (f.comp g).withTop = f.withTop.comp g.withTop

def SupHom.withBot {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) : SupBotHom (WithBot α) (WithBot β)

Adjoins a ⊥ to the domain and codomain of a SupHom.

@[simp]

theorem SupHom.withBot_toFun {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : SupHom α β) (a✝ : WithBot α) : f.withBot a✝ = WithBot.map (⇑f) a✝

@[simp]

theorem SupHom.withBot_id {α : Type u_1} [SemilatticeSup α] : (SupHom.id α).withBot = SupBotHom.id (WithBot α)

@[simp]

theorem SupHom.withBot_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [SemilatticeSup β] [SemilatticeSup γ] (f : SupHom β γ) (g : SupHom α β) : (f.comp g).withBot = f.withBot.comp g.withBot

def SupHom.withTop' {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] [OrderTop β] (f : SupHom α β) : SupHom (WithTop α) β

Adjoins a ⊤ to the codomain of a SupHom.

@[simp]

theorem SupHom.withTop'_toFun {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] [OrderTop β] (f : SupHom α β) (a : WithTop α) : f.withTop' a = Option.elim a ⊤ ⇑f

def SupHom.withBot' {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] [OrderBot β] (f : SupHom α β) : SupBotHom (WithBot α) β

Adjoins a ⊥ to the domain of a SupHom.

@[simp]

theorem SupHom.withBot'_toFun {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] [OrderBot β] (f : SupHom α β) (a : WithBot α) : f.withBot' a = Option.elim a ⊥ ⇑f

def InfHom.withTop {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) : InfTopHom (WithTop α) (WithTop β)

Adjoins a ⊤ to the domain and codomain of an InfHom.

@[simp]

theorem InfHom.withTop_toFun {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) (a✝ : WithTop α) : f.withTop a✝ = WithTop.map (⇑f) a✝

@[simp]

theorem InfHom.withTop_id {α : Type u_1} [SemilatticeInf α] : (InfHom.id α).withTop = InfTopHom.id (WithTop α)

@[simp]

theorem InfHom.withTop_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeInf α] [SemilatticeInf β] [SemilatticeInf γ] (f : InfHom β γ) (g : InfHom α β) : (f.comp g).withTop = f.withTop.comp g.withTop

def InfHom.withBot {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) : InfHom (WithBot α) (WithBot β)

Adjoins a ⊥ to the domain and codomain of an InfHom.

@[simp]

theorem InfHom.withBot_toFun {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] (f : InfHom α β) (a✝ : WithBot α) : f.withBot a✝ = WithBot.map (⇑f) a✝

@[simp]

theorem InfHom.withBot_id {α : Type u_1} [SemilatticeInf α] : (InfHom.id α).withBot = InfHom.id (WithBot α)

@[simp]

theorem InfHom.withBot_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeInf α] [SemilatticeInf β] [SemilatticeInf γ] (f : InfHom β γ) (g : InfHom α β) : (f.comp g).withBot = f.withBot.comp g.withBot

def InfHom.withTop' {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] [OrderTop β] (f : InfHom α β) : InfTopHom (WithTop α) β

Adjoins a ⊤ to the codomain of an InfHom.

@[simp]

theorem InfHom.withTop'_toFun {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] [OrderTop β] (f : InfHom α β) (a : WithTop α) : f.withTop' a = Option.elim a ⊤ ⇑f

def InfHom.withBot' {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] [OrderBot β] (f : InfHom α β) : InfHom (WithBot α) β

Adjoins a ⊥ to the codomain of an InfHom.

@[simp]

theorem InfHom.withBot'_toFun {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] [OrderBot β] (f : InfHom α β) (a : WithBot α) : f.withBot' a = Option.elim a ⊥ ⇑f

def LatticeHom.withTop {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) : LatticeHom (WithTop α) (WithTop β)

Adjoins a ⊤ to the domain and codomain of a LatticeHom.

@[simp]

theorem LatticeHom.withTop_toFun {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) (a✝ : WithTop α) : f.withTop a✝ = WithTop.map (⇑f) a✝

@[simp]

theorem LatticeHom.coe_withTop {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) : ⇑f.withTop = WithTop.map ⇑f

theorem LatticeHom.withTop_apply {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithTop α) : f.withTop a = WithTop.map (⇑f) a

@[simp]

theorem LatticeHom.withTop_id {α : Type u_1} [Lattice α] : (LatticeHom.id α).withTop = LatticeHom.id (WithTop α)

@[simp]

theorem LatticeHom.withTop_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) : (f.comp g).withTop = f.withTop.comp g.withTop

def LatticeHom.withBot {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) : LatticeHom (WithBot α) (WithBot β)

Adjoins a ⊥ to the domain and codomain of a LatticeHom.

@[simp]

theorem LatticeHom.withBot_toFun {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithBot α) : f.withBot a = f.withBot a

@[simp]

theorem LatticeHom.coe_withBot {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) : ⇑f.withBot = WithBot.map ⇑f

theorem LatticeHom.withBot_apply {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithBot α) : f.withBot a = WithBot.map (⇑f) a

@[simp]

theorem LatticeHom.withBot_id {α : Type u_1} [Lattice α] : (LatticeHom.id α).withBot = LatticeHom.id (WithBot α)

@[simp]

theorem LatticeHom.withBot_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) : (f.comp g).withBot = f.withBot.comp g.withBot

def LatticeHom.withTopWithBot {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) : BoundedLatticeHom (WithTop (WithBot α)) (WithTop (WithBot β))

Adjoins a ⊤ and ⊥ to the domain and codomain of a LatticeHom.

@[simp]

theorem LatticeHom.withTopWithBot_toFun {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) (a✝ : WithTop (WithBot α)) : f.withTopWithBot a✝ = WithTop.map (WithBot.map ⇑f) a✝

@[simp]

theorem LatticeHom.coe_withTopWithBot {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) : ⇑f.withTopWithBot = WithTop.map (WithBot.map ⇑f)

theorem LatticeHom.withTopWithBot_apply {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (f : LatticeHom α β) (a : WithTop (WithBot α)) : f.withTopWithBot a = WithTop.map (WithBot.map ⇑f) a

@[simp]

theorem LatticeHom.withTopWithBot_id {α : Type u_1} [Lattice α] : (LatticeHom.id α).withTopWithBot = BoundedLatticeHom.id (WithTop (WithBot α))

@[simp]

theorem LatticeHom.withTopWithBot_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Lattice α] [Lattice β] [Lattice γ] (f : LatticeHom β γ) (g : LatticeHom α β) : (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot

def LatticeHom.withTop' {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [OrderTop β] (f : LatticeHom α β) : LatticeHom (WithTop α) β

Adjoins a ⊥ to the codomain of a LatticeHom.

@[simp]

theorem LatticeHom.withTop'_toFun {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [OrderTop β] (f : LatticeHom α β) (a : WithTop α) : f.withTop' a = Option.elim a ⊤ ⇑f

def LatticeHom.withBot' {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [OrderBot β] (f : LatticeHom α β) : LatticeHom (WithBot α) β

Adjoins a ⊥ to the domain and codomain of a LatticeHom.

@[simp]

theorem LatticeHom.withBot'_toFun {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [OrderBot β] (f : LatticeHom α β) (a : WithBot α) : f.withBot' a = Option.elim a ⊥ ⇑f

def LatticeHom.withTopWithBot' {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [BoundedOrder β] (f : LatticeHom α β) : BoundedLatticeHom (WithTop (WithBot α)) β

Adjoins a ⊤ and ⊥ to the codomain of a LatticeHom.

@[simp]

theorem LatticeHom.withTopWithBot'_toFun {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] [BoundedOrder β] (f : LatticeHom α β) (a : WithTop (WithBot α)) : f.withTopWithBot' a = Option.elim a ⊤ ⇑f.withBot'