Commit 2023-11-01 00:15 370c9af7

View on Github →

chore(Data/Set/Image): re-use some variables (#8054) This also generalizes a universe from Type to Sort in Set.range_eval

Estimated changes

Modified Mathlib/Data/Set/Image.lean

modified theorem Set.preimage_subtype_coe_eq_compl

modified theorem Set.range_eval

modified theorem Set.subsingleton_of_image

modified theorem Set.subsingleton_of_preimage