extend_symm_preimage_inter_range_eventuallyEq

English

The coe (embedding) of extChartAt equals the composition of I with the chart at the point; this shows how extChartAt identifies with the standard chart precomposed with I.

Русский

Встроенная карта extChartAt эквивалентна композиции I с картой в точке; это демонстрирует соответствие extChartAt стандартной карте.

LaTeX

$$$\\mathrm{extChartAt}(I, x) = (I) \\circ (\\mathrm{chartAt}\\,H\\,x)$$$

Lean4

theorem extend_symm_preimage_inter_range_eventuallyEq {s : Set M} {x : M} (hs : s ⊆ f.source) (hx : x ∈ f.source) :
    ((f.extend I).symm ⁻¹' s ∩ range I : Set _) =ᶠ[𝓝 (f.extend I x)] f.extend I '' s := by
  rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin _ hx, map_extend_nhdsWithin_eq_image_of_subset _ hx hs]

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