Naming of docs#IsChain.symm

Stream: mathlib4

[Anne Baanen]

The family of lemmas like docs#IsChain.symm docs#IsAntichain.symm etc includes "symm" in the name but has as type IsChain r s -> IsChain (flip r) s. I think IsChain.flip is slightly less surprising. Is this choice documented somewhere?