mem_toOpenPartialHomeomorph_source

English

The base point a lies in the domain (source) of the local open partial homeomorph built from f at a.

Русский

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

LaTeX

$$$ a \in \operatorname{Dom}(hf.toOpenPartialHomeomorph f) $$$

Lean4

theorem mem_toOpenPartialHomeomorph_source (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    a ∈ (hf.toOpenPartialHomeomorph f).source :=
  (Classical.choose_spec hf.approximates_deriv_on_open_nhds).1

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