LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

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.

A $C^{1}$ map is locally Lipschitz on compact coordinate subsets

Statement

Let $F : M \to N$ be $C^{1}$ , let $(U, φ)$ be a chart on $M$ , let $(V, ψ)$ be a chart on $N$ with $F (U) \subseteq V$ , and let $K \subseteq U$ be compact. Then every point of $K$ has an open neighbourhood $W \subseteq U$ with $\overline{W} \subseteq U$ such that the coordinate representative $ψ \circ F \circ φ^{- 1}$ is Lipschitz on $φ (\overline{W})$ .

Facts & Assumptions

Given: A $C^{1}$ map $F : M \to N$ , charts $(U, φ)$ and $(V, ψ)$ with $F (U) \subseteq V$ , and a compact set $K \subseteq U$ .

[F1]

A $C^{1}$ map has a $C^{1}$ coordinate representative between Euclidean chart domains ( $C^{r}$ and smooth maps between smooth manifolds).

[L1]

A continuous real-valued function on a compact metric space attains a maximum (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[L2]

On a convex Euclidean set, a bound on the derivative norm gives a Lipschitz bound (On a convex open set, a uniform bound $∥ D f (z) v ∥_{2} \leq M ∥ v ∥_{2}$ implies $∥ f (y) - f (x) ∥_{2} \leq M ∥ y - x ∥_{2}$ ).

Proof

technique · direct

1.1

Let $f : = ψ \circ F \circ φ^{- 1}$ . By [F1], $f$ is $C^{1}$ on the open set $φ (U) \subseteq R^{m}$ . For each $x \in φ (K)$ choose an open Euclidean ball $B_{x}$ with $\overline{B_{x}}$ compact and contained in $φ (U)$ .

F1givenchoose

2.1

The derivative norm $∥ D f ∥$ is continuous on each compact ball $\overline{B_{x}}$ , so [L1] gives a finite bound $L_{x}$ there. Since $\overline{B_{x}}$ is convex, [L2] makes $f$ $L_{x}$ -Lipschitz on $\overline{B_{x}}$ .

L1L2step 1.1

3.1

Put $W_{x} : = φ^{- 1} (B_{x})$ . Then $W_{x}$ is an open neighbourhood of $φ^{- 1} (x)$ with $\overline{W_{x}} \subseteq U$ , and $f$ is Lipschitz on $φ (\overline{W_{x}}) = \overline{B_{x}}$ . Since $x$ was arbitrary in $φ (K)$ , the claim follows.

step 2.1construct∎

Depends on

Used by

C¹ local diffeomorphisms preserve null sets locally Lemma
An equidimensional C¹ map sends null sets to null sets Proposition

Dependency tree · two levels

31 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

Marco Gualtieri, Topology I: Smooth Manifolds, cumulative notes (standard reference, not scraped)

A C1C1 map is locally Lipschitz on compact coordinate subsets