English
Let G be a LocalInvariantProp G G' P. For any open subset U of M, any map f: M → M', and any x ∈ U, the property LiftPropAt P f x is equivalent to LiftPropAt P (f ∘ Subtype.val) x, i.e., passing to the subtype does not change the local invariant property at x.
Русский
Пусть G обладает локальной инвариантной пропозицией G и P. Для любого открытого подмножества U ⊆ M, любой отображения f: M → M' и любого x ∈ U, свойство LiftPropAt P f x эквивалентно LiftPropAt P (f ∘ Subtype.val) x, то есть переход к подтипу не изменяет локальное инвариантное свойство в точке x.
LaTeX
$$$ \forall {H M H' M'} {P : (H \to H') \to Set H \to H \to Prop} (hG : LocalInvariantProp G G P) {U : Opens M} (f : M \to M') (x : U),\ LiftPropAt P f x \iff \ LiftPropAt P (f \circ Subtype.val) x.$$$
Lean4
theorem liftPropAt_iff_comp_subtype_val (hG : LocalInvariantProp G G' P) {U : Opens M} (f : M → M') (x : U) :
LiftPropAt P f x ↔ LiftPropAt P (f ∘ Subtype.val) x :=
by
simp only [LiftPropAt, liftPropWithinAt_iff']
congrm ?_ ∧ ?_
· simp_rw [continuousWithinAt_univ, U.isOpenEmbedding'.continuousAt_iff]
· apply hG.congr_iff
exact (U.chartAt_subtype_val_symm_eventuallyEq).fun_comp (chartAt H' (f x) ∘ f)
