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.
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
.
Equations
Instances For
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
.
Equations
Instances For
A version of Equiv.optionCongr
for WithTop
.
Equations
Instances For
A version of Equiv.optionCongr
for WithBot
.
Equations
Instances For
Adjoins a ⊤
to the domain and codomain of a SupHom
.
Equations
Instances For
Adjoins a ⊥
to the domain and codomain of a SupHom
.
Equations
Instances For
Adjoins a ⊤
to the codomain of a SupHom
.
Equations
Instances For
Adjoins a ⊥
to the domain of a SupHom
.
Equations
Instances For
Adjoins a ⊤
to the domain and codomain of an InfHom
.
Equations
Instances For
Adjoins a ⊥
to the domain and codomain of an InfHom
.
Equations
Instances For
Adjoins a ⊤
to the codomain of an InfHom
.
Equations
Instances For
Adjoins a ⊥
to the codomain of an InfHom
.
Equations
Instances For
Adjoins a ⊤
to the domain and codomain of a LatticeHom
.
Equations
Instances For
Adjoins a ⊥
to the domain and codomain of a LatticeHom
.
Equations
Instances For
Adjoins a ⊤
and ⊥
to the domain and codomain of a LatticeHom
.
Equations
Instances For
Adjoins a ⊥
to the codomain of a LatticeHom
.
Equations
Instances For
Adjoins a ⊥
to the domain and codomain of a LatticeHom
.
Equations
Instances For
Adjoins a ⊤
and ⊥
to the codomain of a LatticeHom
.