Theorem Set.rangeFactorization_surjective

Modification history

2025-10-27 02:53

Mathlib/Data/Set/Image.lean

feat: characterise when `Set.rangeFactorization` is injective (#30126)

Modified Set.rangeFactorization_surjective View on Github →

2025-08-23 20:29

Mathlib/Data/Set/Image.lean

chore: rename `Set.surjective_onto_image` (#28627) …

Added Set.rangeFactorization_surjective View on Github →