contDiffAt_map_inverse — Mathlib

English

If e is a continuous linear equivalence between Banach spaces, then the map inverse is C^n at e.

Русский

Если e — непрерывное линейное взаимно однозначное отображение между банаховыми пространствами, то отображение обратного является C^n в точке e.

LaTeX

$$$\\mathrm{ContDiffAt}_{\\mathbb{k}}\\ n\\ \\text{inverse}\\ e$ for $e : E \\to_L[F] G$ with completeness assumptions.$$

Lean4

/-- At an invertible map `e : M →L[R] M₂` between Banach spaces, the operation of
inversion is `C^n`, for all `n`. -/
theorem contDiffAt_map_inverse [CompleteSpace E] {e : E →L[𝕜] F} (he : e.IsInvertible) : ContDiffAt 𝕜 n inverse e :=
  by
  rcases he with ⟨M, rfl⟩
  exact _root_.contDiffAt_map_inverse M

Похожие утверждения