Stream: math-comp analysis

Topic: complete lattice

view this post on Zulip vlj (Aug 26 2020 at 18:46):

Is there a formalisation of complete lattice ? I initially though that the C in CTBDistrLattice stood for Complete, but it's actually for Complement.

view this post on Zulip Karl Palmskog (Aug 26 2020 at 18:50):

here are complete lattices in MathComp, but done in a different way than the other order MC stuff (the formalization precedes order.v): https://github.com/TyGuS/htt/blob/master/Core/domain.v

view this post on Zulip vlj (Sep 12 2020 at 21:51):

thanks !

Last updated: Apr 19 2024 at 11:02 UTC