Bounded lattice


Definition

ProofWiki

Axioms

      sup_comm: ?x \(\sqcup\) ?y = ?y \(\sqcup\) ?x
      inf_comm: ?x \(\sqcap\) ?y = ?y \(\sqcap\) ?x

     sup_assoc: (?x \(\sqcup\) ?y) \(\sqcup\) ?z = ?x \(\sqcup\) (?y \(\sqcup\) ?z)
     inf_assoc: (?x \(\sqcap\) ?y) \(\sqcap\) ?z = ?x \(\sqcap\) (?y \(\sqcap\) ?z)

      sup_idem: ?x \(\sqcup\) ?x
      inf_idem: ?x \(\sqcap\) ?x

sup_inf_absorb: ?x \(\sqcup\) (?x \(\sqcap\) ?y) = ?x
inf_sup_absorb: ?x \(\sqcap\) (?x \(\sqcup\) ?y) = ?x

 sup_bot_right: ?x \(\sqcup\) \(\bot\) = ?x
  sup_bot_left: \(\bot\) \(\sqcup\) ?x = ?x

 inf_top_right: ?x \(\sqcap\) \(\top\) = ?x
  inf_top_left: \(\top\) \(\sqcap\) ?x = ?x