Commit 2025-03-29 19:12 2f2da02a

View on Github →

chore: golf lt_csSup_iff (#23434) The new proof demonstrates to the reader that it's easier to directly use IsLUB/IsGLB than sSup/sInf.

Estimated changes

modified theorem csInf_lt_iff
modified theorem lt_csSup_iff