Commit 2025-07-31 16:18 bfadd55b

View on Github →

feat: f '' s = f ⁻¹' s for an involution f (#27746)

Estimated changes

Modified Mathlib/Data/Set/Image.lean

added theorem Function.Involutive.image_eq_preimage