English
Given a property P on germs in model space, define a corresponding property on sets in a charted space by requiring P holds in every chart around each point.
Русский
Для свойства P над локальными образованиями в модели задаем соответствующее свойство на множествах в диаграмме пространства, требуя соблюдения в каждой карте около каждой точки.
LaTeX
$$$ChartedSpace.LiftPropOn P f s := \forall x \in s, LiftPropWithinAt P f s x$$$
Lean4
/-- Given a property of germs of functions and sets in the model space, then one defines
a corresponding property of functions on sets in a charted space, by requiring that it holds
around each point of the set, in the preferred charts. -/
def LiftPropOn (P : (H → H') → Set H → H → Prop) (f : M → M') (s : Set M) :=
∀ x ∈ s, LiftPropWithinAt P f s x
