liftPropAt_iff — Mathlib

English

The equivalence for LiftPropAt in charts reduces to LiftPropWithinAt.

Русский

Эквивалентность LiftPropAt в диаграммах сводится к LiftPropWithinAt.

LaTeX

$$$ChartedSpace.LiftPropAt P f x \iff ChartedSpace.LiftPropWithinAt P f univ x$$$

Lean4

theorem liftPropAt_iff {P : (H → H') → Set H → H → Prop} {f : M → M'} {x : M} :
    LiftPropAt P f x ↔ ContinuousAt f x ∧ P (chartAt H' (f x) ∘ f ∘ (chartAt H x).symm) univ (chartAt H x x) := by
  rw [LiftPropAt, liftPropWithinAt_iff', continuousWithinAt_univ, preimage_univ]

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