Stream: math-comp users

Topic: Declaring dual structure

view this post on Zulip Evgeniy Moiseenko (Jun 08 2022 at 10:20):

Is there any idiom in mathcomp on how to declare a dual structure, containing all the definitions and lemmas as original one, without just copy-pasting it?

As a concrete example, I need to work with partial orders that have finite ideals:

Now I want to declare dual structure of partial orders with finite filters.
I want to obtain the same set of definitions and lemmas for the dual structure (modulo renaming s/ideal/filter).

Last updated: Jul 15 2024 at 20:02 UTC