Boundaries of regular scalar superlevel sets

A continuous real-valued function whose derivative does not vanish on a level has that level as the frontier of its strict superlevel set, whose closure is then the non-strict superlevel set. This identifies the boundary of domains selected by regular values without requiring a choice of normal vector field.

theorem Continuous.frontier_setOf_lt_eq_of_fderiv_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {u : E → ℝ} {t : ℝ} (hu : Continuous u) (hreg : ∀ (x : E), u x = t → fderiv ℝ u x ≠ 0) : frontier {x : E | t < u x} = {x : E | u x = t}

The frontier of a strict superlevel set is its level set if the derivative is nonzero everywhere on that level.

theorem Continuous.closure_setOf_lt_eq_of_fderiv_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {u : E → ℝ} {t : ℝ} (hu : Continuous u) (hreg : ∀ (x : E), u x = t → fderiv ℝ u x ≠ 0) : closure {x : E | t < u x} = {x : E | t ≤ u x}

The closure of a strict superlevel set is the non-strict superlevel set if the derivative is nonzero everywhere on the level.