liftProp_subtype_val — Mathlib

English

Given a LocalInvariantProp G with a universal Q id univ condition, for any open U ⊆ M, the lift property holds for Subtype.val on U.

Русский

Пусть дано локальное инвариантное свойство G с условием Q id univ, тогда для любого открытого подмножества U ⊆ M свойство подъема действительно для Subtype.val на U.

LaTeX

$$$ \forall {H M H' M'} {Q : (H \to H') \to Set H \to H \to Prop} (hG : LocalInvariantProp G G Q) (hQ : \forall y, Q id univ y) (U : Opens M), LiftProp Q (Subtype.val : U \to M).$$$

Lean4

theorem liftProp_subtype_val {Q : (H → H) → Set H → H → Prop} (hG : LocalInvariantProp G G Q) (hQ : ∀ y, Q id univ y)
    (U : Opens M) : LiftProp Q (Subtype.val : U → M) := by
  intro x
  change LiftPropAt Q (id ∘ Subtype.val) x
  rw [← hG.liftPropAt_iff_comp_subtype_val]
  apply hG.liftProp_id hQ

Похожие утверждения