Commit 2022-08-06 01:01 dffc243a
View on Github →feat(order/complete_lattice): add equiv.supr_congr and equiv.supr_comp lemmas (#15852)
Adds these lemmas as easy consequences of the function.surjective versions in order to aid in discovery.
feat(order/complete_lattice): add equiv.supr_congr and equiv.supr_comp lemmas (#15852)
Adds these lemmas as easy consequences of the function.surjective versions in order to aid in discovery.