Theorems · Theorem · global analysis

Convex.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : NormedSpace ℝ F] {s : Set E} {ω : E → E →L[𝕜] F} [CompleteSpace F],
  Convex ℝ s →
    DifferentiableOn ℝ ω s →
      (∀ a ∈ s,
          ∀ x ∈ tangentConeAt ℝ s a,
            ∀ y ∈ tangentConeAt ℝ s a, ((fderivWithin ℝ ω s a) x) y = ((fderivWithin ℝ ω s a) y) x) →
        ∃ f, ∀ a ∈ s, HasFDerivWithinAt f (ω a) s a

If ω is a closed 1-form on a convex set s, then it admits a primitive, a version stated in terms of fderivWithin.

Defined in

Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare

Cited by

1 results in Mathlib

Foundations

Depth 271 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedSpaceNormedSpaceCompleteSpace