mathlib

0c863e98 - refactor(data/set/finite): change type of `set.finite.dependent_image` (#6475)

refactor(data/set/finite): change type of `set.finite.dependent_image` (#6475) The old lemma combined a statement similar to `set.finite.image` with `set.finite.subset`. The new statement is a direct generalization of `set.finite.image`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>