Commit 2025-08-02 07:11 f0b41744

View on Github →

chore: deprecate Set.image_subset (#27287) Set.image_subset is a duplicate of Set.image_mono. It is also a confusing name because it is very different from Set.preimage_subset. The difference with Set.image_mono is that it has f as an explicit argument. However, in 99% of cases this argument can be inferred, so this is not needed. The main change is in Mathlib/Data/Set/Image.lean

Estimated changes

modified theorem Set.smul_set_mono
modified theorem Set.image_subset
modified theorem Set.monotone_image
modified theorem BooleanSubalgebra.map_mono
modified theorem Sublattice.map_mono