Theorems · Theorem · global analysis

Manifold.LiftSourceTargetPropertyAt.congr_of_eventuallyEq

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f g : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop},
  Manifold.IsLocalSourceTargetProperty P →
    Manifold.LiftSourceTargetPropertyAt I J n f x P → f =ᶠ[nhds x] g → Manifold.LiftSourceTargetPropertyAt I J n g x P

If P is monotone w.r.t. restricting domChart and closed under congruence, if f has property P at x and f and g are eventually equal near x, then g has property P at x.

Defined in

Mathlib.Geometry.Manifold.LocalSourceTargetProperty

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceChartedSpaceTopologicalSpaceChartedSpace