Derivatives on countably many levels

A nonzero derivative isolates a real function's level-set point. Consequently the derivative vanishes almost everywhere on the preimage of any countable set of levels, even when that preimage is uncountable.

theorem TauCeti.countable_setOf_eq_and_deriv_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (c : E) : {t : ℝ | f t = c ∧ deriv f t ≠ 0}.Countable

The points of a level set with nonzero derivative are countable, for any real normed space as codomain.

theorem TauCeti.countable_setOf_mem_and_deriv_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (θ : ℝ → E) {S : Set E} (hS : S.Countable) : {t : ℝ | θ t ∈ S ∧ deriv θ t ≠ 0}.Countable

On countably many levels there are only countably many points with nonzero derivative.

theorem Set.Countable.ae_deriv_eq_zero_on_preimage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace ℝ] {S : Set E} (hS : S.Countable) (θ : ℝ → E) (μ : MeasureTheory.Measure ℝ) [MeasureTheory.NullSingletonClass μ] : ∀ᵐ (t : ℝ) ∂μ, θ t ∈ S → deriv θ t = 0

The derivative vanishes almost everywhere on the preimage of countably many levels for any measure vanishing on singletons. No differentiability assumption or countability of the preimage is required.