Commit 2023-02-27 13:48 f213ec28

View on Github →

fix: bad coercions in Data.Set.Image (#2487) The previous spelling of the coercion caused problems down the line. They are now changed to the coercion arrow, which is the preferred spelling.

Estimated changes

modified theorem Subtype.coe_image_subset
modified theorem Subtype.coe_image_univ
modified theorem Subtype.coe_preimage_self
modified theorem Subtype.preimage_coe_compl
modified theorem Subtype.range_coe
modified theorem Subtype.range_coe_subtype