Commit 2023-03-30 09:07 c941bb94
View on Github →feat(data/set/finite): When s ×ˢ t is finite (#18674)
The one non-trivial result is infinite_image2, because it requires only injectivity of the f a and λ a, f a b rather than of the uncurrying of f.