Commit 2024-01-17 13:26 9c865c10

View on Github →

chore(Order/ConditionallyCompleteLattice/Finset): merge duplicate lemmas (#9807)

Estimated changes

modified theorem Finset.inf'_eq_csInf_image
modified theorem Finset.sup'_eq_csSup_image