Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-15 18:06 302eab4f

View on Github →

chore(data/finset/lattice): Protect ambiguous lemmas (#17938) Protect a few finset lemmas that conflict with root ones when finset is open.

Estimated changes

deleted theorem finset.inf_comm
modified theorem finset.inf_le
modified theorem finset.inf_mono
deleted theorem finset.le_inf
deleted theorem finset.le_inf_iff
deleted theorem finset.le_min
modified theorem finset.le_sup
deleted theorem finset.max_le
deleted theorem finset.sup_comm
deleted theorem finset.sup_le
modified theorem finset.sup_mono