Pairs of multilattices defined on the same set
We define a natural ordering on the power set 𝔓(Q) of any finite partial order Q, and we characterize those partial orders Q for which 𝔓(Q) is a distributive lattice under that ordering.
The article continues the formalization of the lattice theory (as structures with two binary operations, not in terms of ordering relations). In the Mizar Mathematical Library, there are some attempts to formalize prime ideals and filters; one series of articles written as decoding [9] proven some results; we tried however to follow [21], [12], and [13]. All three were devoted to the Stone representation theorem [18] for Boolean or Heyting lattices. The main aim of the present article was to bridge...