Commit 2023-07-18 03:33 6dfe3d46

View on Github →

feat: CompletelyDistribLattice (#5238) Adds new CompletelyDistribLattice/CompleteAtomicBooleanAlgebra classes for complete lattices / complete atomic Boolean algebras that are also completely distributive, and removes the misleading claim that CompleteDistribLattice/CompleteBooleanAlgebra are completely distributive.

  • Product/pi/order dual instances for completely distributive lattices, etc.
  • Every complete linear order is a completely distributive lattice.
  • Every atomic complete Boolean algebra is a complete atomic Boolean algebra.
  • Every complete atomic Boolean algebra is indeed (co)atom(ist)ic.
  • Atom(ist)ic orders are closed under pis.
  • All existing types with CompleteDistribLattice instances are upgraded to CompletelyDistribLattice.
  • All existing types with CompleteBooleanAlgebra instances are upgraded to CompleteAtomicBooleanAlgebra. See related discussion on Zulip.

Estimated changes

added theorem Pi.isAtom_iff
added theorem Pi.isAtom_single
added theorem atom_le_iSup
added theorem eq_iff_atom_le_iff
added theorem iInf_le_coatom
added theorem «Prop».isAtom_iff
added theorem «Prop».isCoatom_iff
added theorem compl_le_self
added theorem compl_lt_self
added theorem Prod.fst_bot
added theorem Prod.fst_top
added theorem Prod.snd_bot
added theorem Prod.snd_top
added theorem iInf_iSup_eq
added theorem iSup_iInf_eq
added theorem iSup_iInf_le
added theorem le_iInf_iSup
added theorem compl_ne_self
added theorem le_compl_self
added theorem lt_compl_self
added theorem ne_compl_self