Commit 2021-03-02 19:27 0c863e98
View on Github →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.