liftPropWithinAt_self_target — Mathlib

English

For f : M → H', LiftPropWithinAt P f s x is equivalent to ContinuousWithinAt f s x and P (f ∘ chartAt_H(x).symm) (chartAt_H(x).symm^{-1} s) (chartAt_H x x).

Русский

Для f: M→H' равносильно ContinuousWithinAt и P для выражения через маппинг по целевому чарту.

LaTeX

$$$\mathrm{LiftPropWithinAt}(P,f,s,x) \iff \big( \mathrm{ContinuousWithinAt}(f,s,x) \wedge P( f \circ \mathrm{chartAt}_{H}(x)^{-1}, \mathrm{chartAt}_{H}(x)^{-1}[s], \mathrm{chartAt}_{H}(x)(x) )\big).$$$

Lean4

theorem liftPropWithinAt_self_target {f : M → H'} :
    LiftPropWithinAt P f s x ↔
      ContinuousWithinAt f s x ∧ P (f ∘ (chartAt H x).symm) ((chartAt H x).symm ⁻¹' s) (chartAt H x x) :=
  liftPropWithinAt_iff' ..

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