Stream: math-comp users

Topic: Order on {set T}


view this post on Zulip Florent Hivert (Sep 28 2021 at 18:34):

I notice that there is currently no formalisation of the inclusion order on {set T}. Is there one in the pipeline ? Would you be interrested to have one contributed ? I need an isomorphic one and I realised that I could define mine by isomorphism.

view this post on Zulip Cyril Cohen (Sep 29 2021 at 12:11):

Please do contribute it to order.v.

view this post on Zulip Florent Hivert (Sep 29 2021 at 14:03):

Also, I just noticed that the documentation of Iso mixup IsoLatticeMixin and IsoDistrLatticeMixin and that there is no IsoBLattice, IsoTBLattice and friend... What do you think about a unique IsoLatticeMixin which coerce to the various lattices mixins depending on the structures on the isomorphic lattice. Is this implementable ?

view this post on Zulip Florent Hivert (Sep 29 2021 at 22:11):

I tried and I'm stuck with uniform inheritance condition problem... I'll try again later...

view this post on Zulip Pierre Roux (Sep 30 2021 at 07:45):

Maybe should we wait for HB to do that kind of changes, in order to avoid doing the job twice?

view this post on Zulip Florent Hivert (Oct 01 2021 at 20:45):

I just submitted a PR defining subset order on {set T}. As suggested by @Pierre Roux I'm keeping the Mixin stuff for after HB.


Last updated: Jan 29 2023 at 19:02 UTC