Theorems · Theorem · global analysis

DifferentiableAt.mem_interior_convex_of_surjective_fderiv

∀ {E : Type u_5} {H : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup H]
  [inst_3 : NormedSpace ℝ H] {f : E → H} {x : E},
  DifferentiableAt ℝ f x →
    ∀ {u : Set E},
      u ∈ nhds x →
        ∀ {s : Set H},
          Convex ℝ s →
            IsClosed s →
              (interior s).Nonempty → Set.MapsTo f u s → Function.Surjective ⇑(fderiv ℝ f x) → f x ∈ interior s

If a function f : E → H is differentiable at x, sends a neighbourhood u of x to a closed convex set s with nonempty interior and has surjective differential at x, it must send x to the interior of s.

Defined in

Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace