pt_mem_toOpenPartialHomeomorph_source

English

The distinguished point pt lies in the source of the open partial homeomorphism associated to the implicit function data.

Русский

Рассматриваемая точка pt принадлежит области определения открытого частичного гомоморфизма, связанного с данными неявной функции.

LaTeX

$$pt \in (\text{toOpenPartialHomeomorph}.source)$$

Lean4

theorem pt_mem_toOpenPartialHomeomorph_source : φ.pt ∈ φ.toOpenPartialHomeomorph.source :=
  φ.hasStrictFDerivAt.mem_toOpenPartialHomeomorph_source

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