extChartAt_preimage_mem_nhds' — Mathlib

English

The preimage of an intersection under an extended chart can be rewritten as the intersection of preimages, facilitating derivative estimates.

Русский

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

LaTeX

$$$ (extChartAt I x).symm^{-1}(s \cap t) \cap \mathrm{range}(I) = (extChartAt I x)^{-1}s \cap \mathrm{range}(I) \cap (extChartAt I x)^{-1}t. $$$

Lean4

theorem extChartAt_preimage_mem_nhds' {x x' : M} (h : x' ∈ (extChartAt I x).source) (ht : t ∈ 𝓝 x') :
    (extChartAt I x).symm ⁻¹' t ∈ 𝓝 (extChartAt I x x') :=
  extend_preimage_mem_nhds _ (by rwa [← extChartAt_source I]) ht

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