Structures · Order
Order.Coframe
A coframe, aka complete Brouwer algebra or complete co-Heyting algebra, is a complete lattice
whose ⊔ distributes over ⨅.
- Defined in
- Mathlib.Order.CompleteBooleanAlgebra
- Shape
- One type argument · adds sdiff_le_iff, top_sdiff
Extends2
Extended by1
Forgetful instances
Every Order.Coframe is also a
Concrete types that are instances5
- TopologicalSpace.Closeds
- Sublocale
- Prod
- OrderDual
- Filter
How is a type an instance?
Loading the hierarchy index…
Assumed by48
- iInf_sup_eq
- sup_iInf_eq
- sup_sInf_eq
- iInf_sup_iInf
- iInf_sup_of_monotone
- sInf_sup_eq
- iInf_iSup_of_monotone
- iInf_iSup_of_antitone
- Order.Coframe.toSDiff
- biInf_sup_biInf
- iInf_codisjoint_iff
- Set.Finite.iInf_biSup_of_monotone
- sup_iInf₂_eq
- sInf_codisjoint_iff
- Order.Coframe.toHNot
- sdiff_eq_sInf
- sInf_sup_sInf
- iInf₂_sup_eq
- iInf_sup_of_antitone
- sdiff_iInf_eq
- codisjoint_iInf_iff
- IsCoatom.iInf_le
- biInf_inter_of_pairwise_codisjoint
- Order.Coframe.toDistribLattice
- le_sdiff_iff
- iInf₂_codisjoint_iff
- Prod.instCoframe
- Set.Finite.biSup_iInf_eq
- iSup_sdiff_eq
- Set.Finite.iInf_biSup_of_antitone
- hnot_eq_sInf_codisjoint
- IsCoatom.sInf_le
- Order.Coframe.MinimalAxioms.of
- SupClosed.countableInfClosure
- Set.iInf_iSup_of_antitone
- Pi.instCoframe
- Order.Coframe.toCoheytingAlgebra
- Equiv.coframe
- OrderDual.instFrame
- codisjoint_iInf₂_iff
- Set.iInf_iSup_of_monotone
- sdiff_iSup_eq
- Order.Coframe.top_sdiff
- Function.Injective.coframe
- Order.Coframe.sdiff_le_iff
- iSup_iInf_eq_of_finite
- Order.Coframe.toCompleteLattice
- codisjoint_sInf_iff
Ancestors36
- Bot
- BoundedOrder
- ChainCompletePartialOrder
- CoheytingAlgebra
- CompleteLattice
- CompletePartialOrder
- CompleteSemilatticeInf
- CompleteSemilatticeSup
- ConditionallyCompleteLattice
- ConditionallyCompletePartialOrder
- ConditionallyCompletePartialOrderInf
- ConditionallyCompletePartialOrderSup
- DistribLattice
- GeneralizedCoheytingAlgebra
- GradeBoundedOrder
- GradeMaxOrder
- GradeMinOrder
- GradeOrder
- HNot
- InfSet
- LE
- LT
- Lattice
- Max
- Min
- Nonempty
- OmegaCompletePartialOrder
- OrderBot
- OrderTop
- PartialOrder
- Preorder
- SDiff
- SemilatticeInf
- SemilatticeSup
- SupSet
- Top