Mathlib Map

Theorems · Definition · order theory

BoundedLatticeHom.id

(α : Type u_2) → [inst : Lattice α] → [inst_1 : BoundedOrder α] → BoundedLatticeHom α α

id as a BoundedLatticeHom.

Defined in
Mathlib.Order.Hom.BoundedLattice
Cited by
19 results in Mathlib
Foundations
Depth 8 from the axioms · uses no axioms
Assumes
LatticeBoundedOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

BoundedLatticeHom.asBoolRing_id · cited by 0BoundedLatticeHom.asBoolR…LatticeHom.withBotWithTop_id · cited by 0LatticeHom.withBotWithTop…BoundedLatticeHom.coe_id · cited by 0BoundedLatticeHom.coe_idBddDistLat.hom_id · cited by 0BddDistLat.hom_idLatticeHom.withTopWithBot_id · cited by 0LatticeHom.withTopWithBot…BoundedLatticeHom.comp_id · cited by 0BoundedLatticeHom.comp_idBooleanSubalgebra.map_id · cited by 0BooleanSubalgebra.map_idRingHom.asBoolAlg_id · cited by 0RingHom.asBoolAlg_idBoundedLatticeHom.dual_id · cited by 0BoundedLatticeHom.dual_idBddDistLat.ofHom_id · cited by 0BddDistLat.ofHom_idBoundedLatticeHom.id_apply · cited by 0BoundedLatticeHom.id_applyBoolAlg.hom_id · cited by 0BoolAlg.hom_idBoundedLatticeHom.id_comp · cited by 0BoundedLatticeHom.id_compFinBddDistLat.hom_id · cited by 0FinBddDistLat.hom_idBooleanSubalgebra.comap_id · cited by 0BooleanSubalgebra.comap_idLattice · cited by 916LatticeBoundedOrder · cited by 270BoundedOrderLatticeHom · cited by 192LatticeHomBoundedLatticeHom · cited by 185BoundedLatticeHomBoundedOrderHom · cited by 54BoundedOrderHomLatticeHom.id · cited by 18LatticeHom.idBoundedOrderHom.id · cited by 8BoundedOrderHom.idBoundedLatticeHom.idCITED BYCITES

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by19

Results whose statement or proof uses this declaration.