Theorems · Definition · functional analysis
Differentiable
(𝕜 : Type u_1) →
[inst : NontriviallyNormedField 𝕜] →
{E : Type u_2} →
[inst_1 : AddCommGroup E] →
[Module 𝕜 E] →
[TopologicalSpace E] →
{F : Type u_3} → [inst_4 : AddCommGroup F] → [Module 𝕜 F] → [TopologicalSpace F] → (E → F) → PropDifferentiable 𝕜 f means that f is differentiable at any point.
- Defined in
- Mathlib.Analysis.Calculus.FDeriv.Defs
- Cited by
- 298 results in Mathlib
- Foundations
- Depth 62 from the axioms, rests on 890 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- DifferentiableAtproof · cited by 617
Cited by298
Results whose statement or proof uses this declaration.
- Differentiable.differentiableOnstatement and proof · cited by 40
- differentiable_idstatement · cited by 35
- Differentiable.differentiableAtstatement and proof · cited by 32
- Differentiable.continuousstatement and proof · cited by 28
- ContinuousLinearMap.differentiablestatement · cited by 18
- Differentiable.compstatement and proof · cited by 17
- ContDiff.differentiablestatement · cited by 15
- Differentiable.diffContOnClstatement and proof · cited by 15
- differentiable_conststatement · cited by 14
- differentiableOn_univstatement · cited by 10
- Differentiable.mulstatement and proof · cited by 9
- Differentiable.addstatement and proof · cited by 8
Showing the 200 most cited of 298.