Commit 2026-01-19 08:37 c3c2870c
View on Github →feat: lemmas to change variables in iSup / iInf / iUnion / iInter over a set (#33844)
Add some lemmas to change variables in iSup / iInf when the index ranges over a set. There are similar lemmas in the Equiv and Function.Surjective namespaces but these are over a whole type.