Commit 2024-07-16 20:08 2422cb56

View on Github →

chore(Order): More simp lemmas (#13338) These lemmas are needed in #13201

Estimated changes

modified theorem isGLB_singleton
modified theorem isGreatest_singleton
modified theorem isLUB_singleton
modified theorem isLeast_singleton
deleted theorem monotone_sInf_of_monotone
deleted theorem monotone_sSup_of_monotone
added theorem OrderHom.mk_comp_mk