Fiber sums of injective maps

Summing along the fibers of an injective map extends a function by zero off the image. This identifies fiber sums with Function.extend, allowing its measurability API to be used.

theorem Function.Injective.tsum_fiber_eq_extend {α : Type u_1} {β : Type u_2} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {f : α → β} (hf : Injective f) (g : α → M) (y : β) : ∑' (x : ↑(f ⁻¹' {y})), g ↑x = extend f g 0 y

A fiber sum along an injective map is the extension by zero of the summand.