Commit 2025-08-23 20:29 24f66283

View on Github →

chore: rename Set.surjective_onto_image (#28627) Rename Set.surjective_onto_image to Set.imageFactorization_surjective. This matches better with other theorems like Set.restrictPreimage_surjective. Also rename Set.surjective_onto_range similarly. I was looking on loogle today and noticed this one again, which doesn't fit any of the naming conventions. I decided to fix it this time.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean

Modified Mathlib/Data/Finite/Card.lean

Modified Mathlib/Data/Set/Countable.lean

Modified Mathlib/Data/Set/Image.lean

added theorem Set.imageFactorization_surjective

added theorem Set.rangeFactorization_surjective

deleted theorem Set.surjective_onto_image

deleted theorem Set.surjective_onto_range

Modified Mathlib/Logic/Small/Set.lean

Modified Mathlib/MeasureTheory/Constructions/Polish/Basic.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

Modified Mathlib/Order/Filter/Finite.lean

Modified Mathlib/Order/SupIndep.lean

Modified Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean

Modified Mathlib/RingTheory/Localization/AsSubring.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Finite.lean

Modified Mathlib/Topology/NoetherianSpace.lean