Theorems · Theorem · global analysis
DifferentiableAt.norm_sq
∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
[inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E}
{x : G}, DifferentiableAt ℝ f x → DifferentiableAt ℝ (fun y => ‖f y‖ ^ 2) x- Cited by
- 1 results in Mathlib
- Foundations
- Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- Norm.normstatement · cited by 5,413
- InnerProductSpacestatement and proof · cited by 3,523
- RCLikestatement and proof · cited by 2,829
- one_ne_zeroproof · cited by 885
- DifferentiableAtstatement and proof · cited by 617
- DifferentiableAt.compproof · cited by 38
- contDiffAt_idproof · cited by 16
- ContDiffAt.differentiableAtproof · cited by 14
- ContDiffAt.norm_sqproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- Differentiable.norm_sqproof · cited by 1