mathlib

c941bb94 - feat(data/set/finite): When `s ×ˢ t` is finite (#18674)

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`.