Structures · Order

CompletelyDistribLattice

A completely distributive lattice is a complete lattice whose ⨅ and ⨆ distribute over each other.

Defined in: Mathlib.Order.CompleteBooleanAlgebra
Shape: One type argument · adds le_himp_iff, himp_bot, sdiff_le_iff, top_sdiff, iInf_iSup_eq

Open in Mathlib docs

Extends2

Extended by2

Forgetful instances

Every CompletelyDistribLattice is also a

CompleteDistribLattice

Provided automatically by

Concrete types that are instances6

UpperSet
LowerSet
SimpleGraph.Subgraph
SimpleGraph.Finsubgraph
Prod
OrderDual

How is a type an instance?

Loading the hierarchy index…