Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-29 06:46 d95851bc

View on Github →

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.

Estimated changes

deleted theorem finset.coe_le_max_of_mem
modified theorem finset.inf_congr
modified theorem finset.inf_id_set_eq_sInter
modified theorem finset.inf_mono_fun
modified theorem finset.le_inf
added theorem finset.le_max
added theorem finset.le_max_of_eq
deleted theorem finset.le_max_of_mem
added theorem finset.min_le
deleted theorem finset.min_le_coe_of_mem
added theorem finset.min_le_of_eq
deleted theorem finset.min_le_of_mem
modified theorem finset.sup_congr
modified theorem finset.sup_eq_supr
modified theorem finset.sup_le
modified theorem finset.sup_mono_fun