Theorems · Theorem · real analysis
le_minSmoothness
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}, n ≤ minSmoothness 𝕜 n- Cited by
- 23 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NontriviallyNormedField
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- ENatstatement and proof · cited by 4,985
- WithTopstatement and proof · cited by 3,754
- IsRCLikeNormedFieldproof · cited by 104
- minSmoothnessstatement · cited by 50
- minSmoothness_defproof · cited by 7
Cited by23
Results whose statement or proof uses this declaration.
- ContDiffWithinAt.isSymmSndFDerivWithinAtproof · cited by 6
- ContDiffAt.isSymmSndFDerivAtproof · cited by 4
- VectorField.mpullback_mlieBracketWithinproof · cited by 3
- ContMDiffWithinAt.mlieBracketWithin_vectorFieldproof · cited by 3
- inverse_mfderiv_add_leftproof · cited by 2
- inverse_mfderiv_mul_leftproof · cited by 2
- contMDiff_mulInvariantVectorFieldproof · cited by 2
- VectorField.mpullbackWithin_mlieBracketWithin'proof · cited by 2
- extDerivWithin_extDerivWithin_applyproof · cited by 2
- contMDiff_addInvariantVectorFieldproof · cited by 2
- VectorField.leibniz_identity_lieBracketWithinproof · cited by 2
- mdifferentiableAt_mulInvariantVectorFieldproof · cited by 1