Theorem 9.21 — $C'$ is equivalent to continuous partial derivatives

Proved

Rudin.ch09_C1_iff_partials_continuous

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysiscalculus

A mapping $\mathbf{f}$ of an open set $E \subseteq \mathbb{R}^n$ into $\mathbb{R}^m$ is continuously differentiable on $E$ if and only if all its partial derivatives exist on $E$ and are continuous there.

Preamble

import Mathlib

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 9.21: `f` is continuously differentiable on an open set `E` if and only if
all its partial derivatives exist on `E` and are continuous there. -/
theorem ch09_C1_iff_partials_continuous (n m : ℕ) (E : Set (EuclideanSpace ℝ (Fin n)))
    (hE : IsOpen E) (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m)) :
    ContDiffOn ℝ 1 f E ↔
      ∃ D : Fin n → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin m),
        (∀ j : Fin n, ∀ x ∈ E,
          HasDerivAt (fun t : ℝ => f (x + t • EuclideanSpace.single j (1 : ℝ))) (D j x) 0) ∧
        (∀ j : Fin n, ContinuousOn (D j) E) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 9, p. 219, Definition 9.20 and Theorem 9.21

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $n,m \in \mathbb{N}$ , let $E \subseteq \mathbb{R}^n$ be open and let $f : \mathbb{R}^n \to \mathbb{R}^m$ . The following are asserted to be equivalent:

$f$ is continuously differentiable of order $1$ on $E$ (continuously differentiable in the Fréchet sense, relative to $E$ );
there exists a family of functions $D_j : \mathbb{R}^n \to \mathbb{R}^m$ , one for each coordinate index $j \in \{0,\dots,n-1\}$ , such that
for every $j$ and every $x \in E$ , the map $t \mapsto f(x + t e_j)$ is differentiable at $t=0$ with derivative $D_j(x)$ (so $D_j(x)$ is the $j$ -th partial derivative of $f$ at $x$ ), and
every $D_j$ is continuous on $E$ .

The partial derivatives are required to exist at all points of $E$ and to be continuous on $E$ only; the functions $D_j$ are defined on all of $\mathbb{R}^n$ , but unconstrained outside $E$ . Both directions of the equivalence are claimed.

Human review

Endorsed by Community (Bot) · Sep 14, 2026
Endorsed by Lucas · Sep 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 9.21 — C′C'C′ is equivalent to continuous partial derivatives

Theorem 9.21 — $C'$ is equivalent to continuous partial derivatives