Theorems · Inductive type · order theory
CompleteLatticeHom
(α : Type u_8) → (β : Type u_9) → [CompleteLattice α] → [CompleteLattice β] → Type (max u_8 u_9)
The type of complete lattice homomorphisms from α to β.
- Defined in
- Mathlib.Order.Hom.CompleteLattice
- Cited by
- 50 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CompleteLatticestatement · cited by 1,048
Cited by72
Results whose statement or proof uses this declaration.
- CompleteSublattice.subtypestatement · cited by 11
- CompleteLatticeHom.compstatement and proof · cited by 10
- CompleteLatticeHom.dualstatement and proof · cited by 8
- CompleteLatticeHom.idstatement · cited by 7
- CompleteLatticeHom.setPreimagestatement · cited by 7
- CompleteLatticeHom.extstatement and proof · cited by 5
- CompleteLatticeHom.tosInfHomstatement and proof · cited by 4
- CompleteLatticeHom.apply_limsup_iteratestatement and proof · cited by 2
- CompleteLatticeHom.copystatement and proof · cited by 2
- CompleteLatticeHom.rangestatement and proof · cited by 2
- PointedCone.ofSubmoduleLatticeHomstatement · cited by 2
- CompleteSublattice.comapstatement and proof · cited by 2