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):

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

thanks !

Last updated: Jun 25 2024 at 19:01 UTC