image_mem_toOpenPartialHomeomorph_target

English

The image mem lemma ensures f(a) belongs to the target of the inverse construction.

Русский

Лемма о принадлежности образа гарантирует, что f(a) принадлежит целевому множеству обратной конструкции.

LaTeX

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

Lean4

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

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