mem_xxx(_iff)

Stream: mathlib4

[Michael Stoll]

This is a question about nameing coneventions. When I was looking at NumberTheory.SmoothNumbers recently, I noticed lemma names like mem_smoothNumbers whose statement is of the form x ∈ ... ↔ ..., and so I thought that it should really be called mem_..._iff. But then I noticed that there are many other statements of that form whose name does not contain _iff. Using a local copy of loogle, I collected all lemmas with a statement of the form above and counted how many include _iff in the name. The result is : Out of the 203 lemmas found,

• 50 have names including (mostly ending in) _iff
• 3 end in _def
• and the remaining 150 do neither.

My conclusion is that there seems to be a convention (which is probably not formally stated anywhere) that such lemmas do not need to be named mem_xxx_iff, but mem_xxx is OK. So I will not rename the lemmas in the file mentioned at the beginning. But I would still like to know if a conscious decision has been made at some point in favor of the non-_iff version.

[Yury G. Kudryashov]

In some cases, first someone added a non-iff lemma, then someone else upgraded it to an iff lemma adding _iff to the name. Then in some cases the first lemma was removed from the library.

[Yury G. Kudryashov]

E.g., I'm upgrading some lemmas to iff now in a local branch but I'm going to leave old lemmas for a while (and deprecate them) for backward compatibility.

[Michael Stoll]

OK, so the point is to disambiguate between implications and equivalences when both are there.

[Yaël Dillies]

Yeah, it's the same as adding an _eq prefix. We (mostly) only do it to disambiguate.

[Yaël Dillies]

You'll note the Set API is more opinionated about having the one way implications separately than the Finset API, hence some lemma name mismatches where the Set version is the Finset version + _iff.

[Michael Stoll]

Yeah, it would be nice to have the Set and Finset APIs as parallel as possible. But this would be a lot of work (and would be likely to break a lot downstream when names change...).