extChartAt_symm_preimage_inter_range_eventuallyEq

English

Under continuous coordinate change, the eventual equality of the two restricted neighborhoods holds along 𝓝 (extChartAt I x x).

Русский

При непрерывном изменении координат существует тождество в пределе для двух ограниченных окрестностей вдоль 𝓝 (extChartAt I x x).

LaTeX

$$$((extChartAt I x).toFun x) \mathrel{.}\mathrm{EventuallyEq} (\text{…}) (\mathcal{N} (extChartAt I x x)).$$$

Lean4

theorem extChartAt_symm_preimage_inter_range_eventuallyEq {f : M → M'} {x : M} (hc : ContinuousWithinAt f s x) :
    ((extChartAt I x).symm ⁻¹' s ∩ range I : Set E) =ᶠ[𝓝 (extChartAt I x x)]
      ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source) : Set E) :=
  by
  rw [← nhdsWithin_eq_iff_eventuallyEq]
  exact hc.nhdsWithin_extChartAt_symm_preimage_inter_range

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