Commit 2025-11-07 10:44 3ec545dd

View on Github →

refactor(Logic/Equiv): rename image_eq_preimage to image_symm_eq_preimage/image_eq_preimage_symm (#31130) The current name was ambiguous on whether the symm came on the LHS or RHS.

Estimated changes

modified theorem Set.subset_smul_set_iff
deleted theorem Flow.image_eq_preimage
modified theorem Equiv.Perm.image_inv
modified theorem Equiv.range_eq_univ
modified theorem MeasurableEquiv.image_symm
added theorem OrderIso.symm_mk
modified theorem Fin.image_rev
modified theorem LowerSet.symm_map
modified theorem UpperSet.symm_map