Theorems · Inductive type · order theory
CompleteDistribLattice
Type u_1 → Type u_1
A complete distributive lattice is a complete lattice whose ⊔ and ⊓ respectively
distribute over ⨅ and ⨆.
- Defined in
- Mathlib.Order.CompleteBooleanAlgebra
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by32
Results whose statement or proof uses this declaration.
- Filter.blimsup_sup_notstatement and proof · cited by 3
- Filter.limsup_piecewisestatement and proof · cited by 2
- Filter.blimsup_or_eq_supstatement and proof · cited by 2
- Filter.sup_liminfstatement and proof · cited by 2
- Filter.sup_limsupstatement and proof · cited by 2
- CompleteDistribLattice.toSDiffstatement and proof · cited by 2
- Filter.limsup_sup_filterstatement and proof · cited by 1
- Filter.blimsup_not_supstatement and proof · cited by 1
- Filter.inf_liminfstatement and proof · cited by 1
- CompleteDistribLattice.toHNotstatement and proof · cited by 1
- Equiv.completeDistribLatticestatement and proof · cited by 0
- Filter.inf_limsupstatement and proof · cited by 0