Theorems · Inductive type · order theory
FrameHom
(α : Type u_8) → (β : Type u_9) → [CompleteLattice α] → [CompleteLattice β] → Type (max u_8 u_9)
The type of frame homomorphisms from α to β. They preserve finite meets and arbitrary joins.
- Defined in
- Mathlib.Order.Hom.CompleteLattice
- Cited by
- 70 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 by102
Results whose statement or proof uses this declaration.
- TopologicalSpace.Opens.comapstatement · cited by 32
- FrameHom.compstatement and proof · cited by 10
- Frm.ofHomstatement and proof · cited by 9
- FrameHom.idstatement · cited by 7
- Frm.Hom.homstatement · cited by 7
- FrameHom.extstatement and proof · cited by 6
- PrimeSpectrum.comap_basicOpenstatement · cited by 4
- TopologicalSpace.IsOpenCover.comapstatement · cited by 4
- Sublocale.restrictstatement · cited by 4
- FrameHom.toInfTopHomstatement and proof · cited by 3
- Submodule.localized₀FrameHomstatement · cited by 3
- AlgebraicGeometry.StructureSheaf.toOpen_comp_comapstatement · cited by 3