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.1

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

given

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.1

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

F1step 1.2

3.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$ .

L2step 2.1

4.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.

step 1.1step 3.1∎

Depends on

Used by

A Morse function on a compact manifold has finitely many critical points Corollary

Dependency tree · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Michele Audin and Mihai Damian, Morse Theory and Floer Homology (standard reference, not scraped)
Ralph L. Cohen, Bundles, Manifolds, and Homotopy (standard reference, not scraped)