image_mem_toOpenPartialHomeomorph_target

English

The point f(a) lies in the target (image) of the local open partial homeomorph attached to f.

Русский

Точка f(a) лежит в образе локального открытого частичного гомоморфизма, связанного с f.

LaTeX

$$$ f(a) \in (hf.toOpenPartialHomeomorph f).{\rm target} $$$

Lean4

theorem image_mem_toOpenPartialHomeomorph_target (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    f a ∈ (hf.toOpenPartialHomeomorph f).target :=
  (hf.toOpenPartialHomeomorph f).map_source hf.mem_toOpenPartialHomeomorph_source

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