Theorems · Theorem · global analysis

preimage_extChartAt_eventuallyEq_compl_singleton

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {s t : Set M} (y : M),
  s =ᶠ[nhdsWithin x {y}ᶜ] t →
    ↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I =ᶠ[nhdsWithin (↑(extChartAt I x) x) {↑(extChartAt I x) x}ᶜ]
      ↑(extChartAt I x).symm ⁻¹' t ∩ Set.range ↑I

If two sets coincide locally around x, except maybe at a point y, then their preimage under extChartAt x coincide locally, except maybe at extChartAt I x x.

Defined in

Mathlib.Geometry.Manifold.MFDeriv.Basic

Cited by

3 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpace