extend_preimage_mem_nhds_of_mem_nhdsWithin

English

If x ∈ f.source and s ∈ 𝓝[range I] (f.extend I x), then the preimage under f.extend I of s belongs to 𝓝 x. This is a basic continuity property of the extended chart.

Русский

Если x ∈ f.source и s ∈ 𝓝[range I](f.extend I x), то обратная карта f.extend I^{-1} примененная к s принадлежит 𝓝 x.

LaTeX

$$$s \\in 𝓝[\\mathrm{range}\\, I](f^{\\mathrm{ext}}(x)) \\implies (f^{\\mathrm{ext}})^{-1}(s) \\in 𝓝 x$$$

Lean4

theorem extend_preimage_mem_nhds_of_mem_nhdsWithin {s : Set E} {x : M} (hx : x ∈ f.source)
    (hs : s ∈ 𝓝[range I] (f.extend I x)) : (f.extend I) ⁻¹' s ∈ 𝓝 x := by rwa [← map_extend_nhds (I := I) f hx] at hs

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