liftPropAt_of_mem_groupoid — Mathlib

English

If G LocalInvariantProp, hQ holds for all y, and e ∈ maximalAtlas M G, then LiftPropAt Q e x for all x in e.source.

Русский

Если локальная инвариантность и hQ верны для всех y, и e принадлежит максимальному атласу, то LiftPropAt Q e x верно для всех x из source e.

LaTeX

$$LiftPropAt Q e x$$

Lean4

theorem liftPropAt_of_mem_groupoid (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y)
    {f : OpenPartialHomeomorph H H} (hf : f ∈ G) {x : H} (hx : x ∈ f.source) : LiftPropAt Q f x :=
  liftPropAt_of_mem_maximalAtlas hG hQ (G.mem_maximalAtlas_of_mem_groupoid hf) hx

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