Commit 2024-01-06 09:51 cd6e906e

View on Github →

chore(Set/Function): don't use Sort _ (#9478) Use Sort* or Type* instead. Also slightly golf 1 proof.

Estimated changes

Modified Mathlib/Data/Set/Function.lean

modified theorem Function.antitoneOn_of_rightInvOn_of_mapsTo

modified theorem Function.monotoneOn_of_rightInvOn_of_mapsTo

modified theorem Function.update_comp_eq_of_not_mem_range'

modified theorem Function.update_comp_eq_of_not_mem_range