mathlib
4d06b17a - chore(data/set/intervals/monotone): fix names (#18924)

Commit
2 years ago
chore(data/set/intervals/monotone): fix names (#18924) Some lemmas used `Iic` instead of `Ici` in the names, probably because of a copy+paste error.
Author
Parents
Loading