English
Let P be a property of germs of maps between model spaces H → H' and sets in H. The lifted property of a map f : M → M' between charted spaces is defined by requiring that, around every point x ∈ M, the coordinate expression of f (in the chart at x and the chart at f(x)) satisfies P on all of the model space.
Русский
Пусть P — свойство локальных каскадов отображений между моделями H → H' и множествами в H. Поднятое свойство отображения f : M → M' между хартированными пространствами определяется так, чтобы в окрестности каждой точки x ∈ M координатное выражение f в рамках графы x и графы f(x) удовлетворяло свойству P на всей модели.
LaTeX
$$$\mathrm{LiftProp}(P,f) \equiv \forall x,\ \mathrm{LiftPropAt}(P,f,x)$$$
Lean4
/-- Given a property of germs of functions and sets in the model space, then one defines
a corresponding property of a function in a charted space, by requiring that it holds
in the preferred chart around every point. -/
def LiftProp (P : (H → H') → Set H → H → Prop) (f : M → M') :=
∀ x, LiftPropAt P f x
