Commit 2021-06-13 11:45 6d2a0512View on Github →
feat(algebra/covariant_and_contravariant): API for covariant_and_contravariant (#7889)
This PR introduces more API for
contravariant stuff .
Besides the API, I have not actually made further use of the typeclasses or of the API. This happens in subsequent PRs.
This is a step towards PR #7645.
added theorem act_rel_act_of_rel
added theorem act_rel_act_of_rel_of_rel
added theorem act_rel_of_act_rel_of_rel_act_rel
added theorem act_rel_of_rel_of_act_rel
modified def contravariant
added theorem contravariant_flip_mul_iff
added theorem contravariant_lt_of_contravariant_le
added theorem covariant_flip_mul_iff
added theorem covariant_le_iff_contravariant_lt
added theorem covariant_le_of_covariant_lt
added theorem covariant_lt_iff_contravariant_le
added theorem covconv
added theorem group.covariant_iff_contravariant
added theorem rel_act_of_act_rel_act_of_rel_act
added theorem rel_act_of_rel_of_rel_act
added theorem rel_iff_cov
added theorem rel_of_act_rel_act