mathlib
d95851bc - chore(data/finset/lattice): use more common name, fix spaces (#16336)

Commit
3 years ago
chore(data/finset/lattice): use more common name, fix spaces (#16336) `coe_le_max_of_mem` -> `le_max` `le_max_of_mem` -> `le_max_of_eq` `min_le_coe_of_mem` -> `min_le` `min_le_of_mem` -> `min_le_of_eq` `coe_le_max_of_mem` is an analogue of `le_sup` and `min_le_coe_of_mem` is an analogue of `inf_le`, new names are more consistent with them. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Author
Parents
Loading