Commit 2023-12-25 00:48 8919646c

View on Github →

chore(Data/Set/Function): rename some lemmas (#9257)

  • Set.maps_image_to → Set.mapsTo_image_iff;
  • Set.maps_univ_to → Set.mapsTo_univ_iff;
  • Set.maps_range_to → Set.mapsTo_range_iff. In all cases, use implicit arguments instead of explicit arguments. In the last case, also generalize from Type* to Sort* and replace the RHS with its simp-normal form. Old lemmas stay there but are now deprecated.

Estimated changes

added theorem Set.mapsTo_image_iff
added theorem Set.mapsTo_range_iff
added theorem Set.mapsTo_univ_iff
modified theorem Set.maps_image_to