LemmaStatement: Literature-sourcedProof: Literature-sourcedaudited 2026-09-04

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Nondegenerate critical points are isolated

Statement

Let $f : M \to R$ be smooth. Every nondegenerate critical point of $f$ has an open neighbourhood containing no other critical point of $f$ .

Facts & Assumptions

Given: A smooth function $f : M \to R$ and a nondegenerate critical point $p$ of $f$ .

[F1]

A critical point is nondegenerate exactly when its Hessian has trivial kernel (The intrinsic Hessian of a smooth function at a critical point, Nondegenerate critical points, nullity, index, and coindex).

[L1]

In coordinates $x = (x^{1}, \dots, x^{n})$ , $d f_{q} = \sum_{i} \frac{\partial (f \circ x^{- 1})}{\partial x^{i}} (x (q)) d x_{q}^{i} .$ (Coordinate formula for the differential of a function)

[L2]

A $C^{1}$ map $R^{n} \to R^{n}$ with invertible derivative at a point is a local diffeomorphism there (The Euclidean inverse function theorem).

Proof

technique · dimension split

1.1given

If $\dim M = 0$ , then ${p}$ is open in $M$ , so it already contains no other point and hence no other critical point.

1.2

Assume $\dim M = n > 0$ . Choose a chart $x : U \to R^{n}$ with $x (p) = 0$ , write $g : = f \circ x^{- 1}$ , and define $G (u) : = (\partial_{1} g (u), \dots, \partial_{n} g (u))$ . By [L1], for $q \in U$ one has $d f_{q} = 0$ exactly when $G (x (q)) = 0$ . [L1, given, assume-case[ positive-dimension], construct]

2.1F1step 1.2

The derivative $D G (0)$ is the Hessian matrix of $g$ at $0$ , and [F1] makes it invertible because $p$ is nondegenerate.

3.1L2step 2.1

Applying [L2] to $G$ at $0$ gives a neighbourhood $W$ of $0$ in which $G^{- 1} (0) = {0}$ . Therefore the corresponding neighbourhood $x^{- 1} [W] \subseteq U$ contains no critical point except $p$ .

4.1step 1.1step 3.1∎

The zero-dimensional case is step 1.1, and the positive-dimensional case is step 3.1. Hence every nondegenerate critical point is isolated.

Nondegenerate critical points are isolated

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources