Theorems · Theorem · ordinary differential equations
hasDerivAt_gronwallBound
∀ (δ K ε x : ℝ), HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
- Defined in
- Mathlib.Analysis.ODE.Gronwall
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 186 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites25
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
- TopologicalSpaceproof · cited by 24,529
- Moduleproof · cited by 20,661
- AddCommGroupproof · cited by 12,871
- NontriviallyNormedFieldproof · cited by 8,742
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- Nat.cast_oneproof · cited by 2,501
- zero_addproof · cited by 2,366
- MulZeroClass.zero_mulproof · cited by 1,625
- ContinuousSMulproof · cited by 1,016
- one_ne_zeroproof · cited by 885
Cited by1
Results whose statement or proof uses this declaration.
- hasDerivAt_gronwallBound_shiftproof · cited by 1