Structures · Order
CompleteDistribLattice
A complete distributive lattice is a complete lattice whose ⊔ and ⊓ respectively
distribute over ⨅ and ⨆.
- Defined in
- Mathlib.Order.CompleteBooleanAlgebra
- Shape
- One type argument · adds sdiff_le_iff, top_sdiff
Extends3
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances2
- Prod
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by27
- Filter.blimsup_sup_not
- Filter.blimsup_or_eq_sup
- Filter.limsup_piecewise
- Filter.sup_liminf
- Filter.sup_limsup
- CompleteDistribLattice.toSDiff
- CompleteDistribLattice.toHNot
- Filter.blimsup_not_sup
- Filter.limsup_sup_filter
- Filter.inf_liminf
- CompleteDistribLattice.toFrame
- Prod.instCompleteDistribLattice
- Filter.inf_limsup
- Filter.bliminf_not_inf
- Filter.bliminf_or_eq_inf
- Filter.bliminf_inf_not
- CompleteDistribLattice.MinimalAxioms.of
- Pi.instCompleteDistribLattice
- OrderDual.instCompleteDistribLattice
- CompleteDistribLattice.top_sdiff
- CompleteDistribLattice.toCoframe
- Filter.liminf_piecewise
- CompleteDistribLattice.toBiheytingAlgebra
- Equiv.completeDistribLattice
- CompleteDistribLattice.sdiff_le_iff
- Filter.liminf_sup_filter
- Function.Injective.completeDistribLattice
Ancestors43
- BiheytingAlgebra
- Bot
- BoundedOrder
- ChainCompletePartialOrder
- CoheytingAlgebra
- Compl
- CompleteLattice
- CompletePartialOrder
- CompleteSemilatticeInf
- CompleteSemilatticeSup
- ConditionallyCompleteLattice
- ConditionallyCompletePartialOrder
- ConditionallyCompletePartialOrderInf
- ConditionallyCompletePartialOrderSup
- DistribLattice
- GeneralizedCoheytingAlgebra
- GeneralizedHeytingAlgebra
- GradeBoundedOrder
- GradeMaxOrder
- GradeMinOrder
- GradeOrder
- HImp
- HNot
- HeytingAlgebra
- InfSet
- LE
- LT
- Lattice
- Max
- Min
- Nonempty
- OmegaCompletePartialOrder
- Order.Coframe
- Order.Frame
- OrderBot
- OrderTop
- PartialOrder
- Preorder
- SDiff
- SemilatticeInf
- SemilatticeSup
- SupSet
- Top