Structures · Order
Order.Frame
A frame, aka complete Heyting algebra, is a complete lattice whose ⊓ distributes over ⨆.
- Defined in
- Mathlib.Order.CompleteBooleanAlgebra
- Shape
- One type argument · adds le_himp_iff, himp_bot
Extends2
Extended by1
Forgetful instances
Every Order.Frame is also a
Concrete types that are instances7
- TopologicalSpace.Opens
- Nucleus
- Frm.carrier
- Subtype
- Prod
- OrderDual
- Set.Elem
How is a type an instance?
Loading the hierarchy index…
Assumed by117
- Frm.ofHom
- iSup_inf_eq
- Nucleus.toSublocale
- Sublocale.toNucleus
- inf_sSup_eq
- inf_iSup_eq
- Sublocale.restrict
- iSup_inf_iSup
- iSup_iInf_of_monotone
- disjoint_iSup_iff
- Sublocale.sInf_mem
- Sublocale.carrier
- iSup_inf_of_monotone
- sSup_inf_eq
- biSup_inf_biSup
- himp_eq_sSup
- iSup_iInf_of_antitone
- iInf_iSup_eq_of_finite
- Set.Finite.iSup_biInf_of_monotone
- IsAtom.le_iSup
- sSup_disjoint_iff
- Order.Frame.toHImp
- disjoint_sSup_iff
- iSup_disjoint_iff
- nucleusIsoSublocale
- Order.Frame.toCompl
- Sublocale.sInf_mem'
- compl_eq_sSup_disjoint
- iSup₂_disjoint_iff
- sSupIndep_iff_pairwiseDisjoint
- Nucleus.restrict
- sSup_inf_sSup
- Nucleus.map_himp_le
- Nucleus.comp_eq_right_iff_le
- Nucleus.mem_range
- Sublocale.infClosed
- disjoint_iSup₂_iff
- biSup_inter_of_pairwise_disjoint
- Sublocale.himp_mem'
- Set.Finite.biInf_iSup_eq
- Sublocale.giRestrict
- IsAtom.le_sSup
- iSup_inf_of_antitone
- Sublocale.restrict_of_mem
- Sublocale.range_toNucleus
- inf_iSup₂_eq
- Nucleus.coe_toSublocale
- Locale.of
- Sublocale.toNucleus_apply
- Sublocale.mem_mk
Ancestors36
- Bot
- BoundedOrder
- ChainCompletePartialOrder
- Compl
- CompleteLattice
- CompletePartialOrder
- CompleteSemilatticeInf
- CompleteSemilatticeSup
- ConditionallyCompleteLattice
- ConditionallyCompletePartialOrder
- ConditionallyCompletePartialOrderInf
- ConditionallyCompletePartialOrderSup
- DistribLattice
- GeneralizedHeytingAlgebra
- GradeBoundedOrder
- GradeMaxOrder
- GradeMinOrder
- GradeOrder
- HImp
- HeytingAlgebra
- InfSet
- LE
- LT
- Lattice
- Max
- Min
- Nonempty
- OmegaCompletePartialOrder
- OrderBot
- OrderTop
- PartialOrder
- Preorder
- SemilatticeInf
- SemilatticeSup
- SupSet
- Top