English
If G has LocalInvariantProp G Q and the Q id univ condition holds, then for any inclusion of opens U ≤ V, the lift property holds for Opens.inclusion, i.e., lifting along an inclusion is invariant.
Русский
Если G обладает локальным инвариантным свойством G Q и выполняется Q id univ, то для вложения открытых множеств U ≤ V свойство подъема сохраняется для Opens.inclusion.
LaTeX
$$$ \forall {H M H' M'} {G : StructureGroupoid H} {Q : (H \to H') \to Set H \to H \to Prop} (hG : LocalInvariantProp G G Q) (hQ : \forall y, Q id univ y) {U V : Opens M} (hUV : U \le V), LiftProp Q (Opens.inclusion hUV : U \to V).$$$
Lean4
theorem liftProp_inclusion {Q : (H → H) → Set H → H → Prop} (hG : LocalInvariantProp G G Q) (hQ : ∀ y, Q id univ y)
{U V : Opens M} (hUV : U ≤ V) : LiftProp Q (Opens.inclusion hUV : U → V) :=
by
intro x
change LiftPropAt Q (id ∘ Opens.inclusion hUV) x
rw [← hG.liftPropAt_iff_comp_inclusion hUV]
apply hG.liftProp_id hQ
