Theorem differentiableOn_empty

Modification history

2026-02-04 14:37

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

feat: `differentiable_of_subsingleton` (#34831) …

Modified differentiableOn_empty View on Github →

2025-05-27 02:03

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

chore(Analysis/Calculus): split long file FDeriv/Basic.lean (#25207)

Modified differentiableOn_empty View on Github →

2023-05-21 21:51

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

feat: port Analysis.Calculus.FDeriv.Basic (#4132)

Added differentiableOn_empty View on Github →