Images after removing finitely many inputs

For a measure with null singletons, removing finitely many inputs changes the image of an arbitrary map only on a null set. Neither measurability nor injectivity of the map is needed.

theorem Set.Finite.image_sdiff_ae_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace β] {Z : Set α} (hZ : Z.Finite) (f : α → β) (s : Set α) (μ : MeasureTheory.Measure β) [MeasureTheory.NullSingletonClass μ] : f '' s =ᵐ[μ] f '' (s \ Z)

Removing finitely many inputs preserves an arbitrary image almost everywhere for a measure with null singletons.