mem_toOpenPartialHomeomorph_source

English

For ContDiffAt, the target lies in the image under the open partial homeomorph.

Русский

Для ContDiffAt целевой образ лежит в образе открытого частичного гомоморфа.

LaTeX

$$$(f a) \in (hf.toOpenPartialHomeomorph f hf' hn).target$$$

Lean4

theorem mem_toOpenPartialHomeomorph_source (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (f' : E →L[𝕂] F) a)
    (hn : 1 ≤ n) : a ∈ (hf.toOpenPartialHomeomorph f hf' hn).source :=
  (hf.hasStrictFDerivAt' hf' hn).mem_toOpenPartialHomeomorph_source

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