Commit 2025-04-24 15:36 acfb1af2

View on Github →

refactor: generalise Finset.isLUB_sup to an arbitrary function (#24325)

Estimated changes

modified theorem Finset.isGLB_inf
added theorem Finset.isGLB_inf_id
modified theorem Finset.isLUB_sup
added theorem Finset.isLUB_sup_id