extend_preimage_mem_nhdsWithin — Mathlib

English

If x ∈ f.source and s ⊆ f.source, then the nhdsWithin of s under the inverse extension maps to 𝓝 x through the preimage by the extended chart.

Русский

Если x ∈ f.source и s ⊆ f.source, то окрестности nhdsWithin по обратной карте отображаются через предобраз в 𝓝 x.

LaTeX

$$$s \\subseteq f.source \\Rightarrow (f^{\\mathrm{ext}})^{-1}[s] \\in 𝓝 x$$$

Lean4

/-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point
in the source is a neighborhood of the preimage, within a set. -/
theorem extend_preimage_mem_nhdsWithin {x : M} (h : x ∈ f.source) (ht : t ∈ 𝓝[s] x) :
    (f.extend I).symm ⁻¹' t ∈ 𝓝[(f.extend I).symm ⁻¹' s ∩ range I] f.extend I x := by
  rwa [← map_extend_symm_nhdsWithin f (I := I) h, mem_map] at ht

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