Measure Theory Helpers for Residue Theory

Countability of isolated point sets and measure-zero results for preimages of singletons under piecewise C¹ immersions.

theorem Set.countable_setOf_isolated_points' {S : Set ℝ} (h : ∀ t ∈ S, ∃ ε > 0, ∀ s ∈ S, s ≠ t → |s - t| ≥ ε) : S.Countable

theorem preimage_singleton_measure_zero_of_deriv_ne_zero {γ : ℝ → ℂ} {a b : ℝ} {P : Finset ℝ} (z₀ : ℂ) (_hγ : ContinuousOn γ (Set.Icc a b)) (hγ_diff : ∀ t ∈ Set.Icc a b, t ∉ P → DifferentiableAt ℝ γ t) (hγ'_ne : ∀ t ∈ Set.Icc a b, t ∉ P → deriv γ t ≠ 0) : MeasureTheory.volume {t : ℝ | t ∈ Set.Icc a b ∧ γ t = z₀} = 0

Preimage of a singleton under a piecewise C¹ immersion has measure zero.