Commit 2026-10-13 08:04 9799b807

View on Github →

feat(Data/PFun): add lemmas for ran, restrict, map, image and preimage (#41830) Add missing simp / API lemmas for partial functions, and strengthen preimage_inter from a subset inclusion to an equality. Also tag a few Part uniqueness lemmas for grind.

  • Part: grind attributes on get_mem, mem_unique, mem_right_unique
  • ran: ran_coe, ran_eq_empty_iff_dom_eq_empty
  • restrict: dom_restrict, restrict_restrict, ran_restrict, preimage_restrict
  • map: dom_map, mem_map, ran_map, image_map, preimage_map
  • image / preimage: image_subset_ran, preimage_empty, disjoint_preimage_of_disjoint, plus simp/gcongr attributes

Estimated changes

added theorem PFun.dom_map
added theorem PFun.dom_restrict
added theorem PFun.image_map
added theorem PFun.image_subset_ran
added theorem PFun.mem_map
added theorem PFun.preimage_empty
modified theorem PFun.preimage_inter
added theorem PFun.preimage_map
added theorem PFun.preimage_restrict
added theorem PFun.ran_coe
added theorem PFun.ran_map
added theorem PFun.ran_restrict
added theorem PFun.restrict_restrict