Commit 2024-12-16 10:17 337fbe4c

View on Github →

refactor(Mathlib/Order): remove duplicate lemma iInf_le' (#19911) Remove iInf_le' which is equal to iInf_le.

Estimated changes

modified theorem iInf_le'
modified theorem le_iSup'