English
LiftProp P f holds exactly when f is continuous and, for every point x, the coordinate expression of f lies in the germ property P on the whole model space.
Русский
Свойство LiftProp P f выполняется тогда и только тогда, когда f непрерывно, и для каждой точки x координатное выражение f удовлетворяет свойству P на всей модели.
LaTeX
$$$\mathrm{LiftProp}(P,f) \iff \Big( \mathrm{Continuous}(f) \wedge \forall x,\; P\big(\mathrm{chartAt}_{H'}(f(x)) \circ f \circ (\mathrm{chartAt}_H(x))^{-1}\big)\, \mathrm{univ} \, (\mathrm{chartAt}_H(x)(x))\Big).$$$
Lean4
theorem liftProp_iff {P : (H → H') → Set H → H → Prop} {f : M → M'} :
LiftProp P f ↔ Continuous f ∧ ∀ x, P (chartAt H' (f x) ∘ f ∘ (chartAt H x).symm) univ (chartAt H x x) := by
simp_rw [LiftProp, liftPropAt_iff, forall_and, continuous_iff_continuousAt]
