liftPropWithinAt_self_source — Mathlib

English

If two source charts e and e' belong to the atlas, and g maps x into the source of f and hG invariance holds, then the property P for the representations via e and via e' are equivalent at x.

Русский

Если два источника-чарта e, e' принадлежат атласу, и g(x) лежит в источнике f, то свойство P для выражений f∘g∘e^{-1} и f∘g∘e'^{-1} одинаково в точке x.

LaTeX

$$$P(f\circ g\circ e^{-1})\big(e^{-1}s\big)\;\text{ at }x \iff P(f'\circ g\circ e'^{-1})\big(e'^{-1}s\big)\text{ at }x.$$$

Lean4

theorem liftPropWithinAt_self_source {f : H → M'} {s : Set H} {x : H} :
    LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (chartAt H' (f x) ∘ f) s x :=
  liftPropWithinAt_iff' ..

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