English
Let G be a LocalInvariantProp G G' P. For open sets U ⊆ M and V ⊆ M such that U ≤ V, and a map f : V → M', the LiftPropAt P f (inclusion) is equivalent to LiftPropAt P (f ∘ inclusion) on U, expressing stability under restriction to an inclusion.
Русский
Пусть G имеет локальное инвариантное свойство G G' P. Для открытых множеств U ⊆ M и V ⊆ M с U ≤ V и отображения f : V → M', свойство LiftPropAt P f (inclusion) эквивалентно LiftPropAt P (f ∘ inclusion) на U, демонстрируя устойчивость к вложению.
LaTeX
$$$ \forall {H M H' M'} {P : (H \to H') \to Set H \to H \to Prop} (hG : LocalInvariantProp G G P) {U V : Opens M} (hUV : U \le V) (f : V \to M'),\ LiftPropAt P f (\mathrm{inclusion}\; hUV) x \iff \ LiftPropAt P (f \circ \mathrm{inclusion}\; hUV) x.$$$
Lean4
theorem liftPropAt_iff_comp_inclusion (hG : LocalInvariantProp G G' P) {U V : Opens M} (hUV : U ≤ V) (f : V → M')
(x : U) : LiftPropAt P f (Set.inclusion hUV x) ↔ LiftPropAt P (f ∘ Set.inclusion hUV : U → M') x :=
by
simp only [LiftPropAt, liftPropWithinAt_iff']
congrm ?_ ∧ ?_
· simp_rw [continuousWithinAt_univ, (TopologicalSpace.Opens.isOpenEmbedding_of_le hUV).continuousAt_iff]
· apply hG.congr_iff
exact
(TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq hUV).fun_comp
(chartAt H' (f (Set.inclusion hUV x)) ∘ f)
