liftPropAt_of_mem_maximalAtlas — Mathlib

English

Let h₁ hold: ∀ y ∈ s, g' y = g y. Then LiftPropOn P g' s ↔ LiftPropOn P g s.

Русский

Пусть выполняется h₁: ∀ y ∈ s, g' y = g y. Тогда LiftPropOn P g' s эквивалентно LiftPropOn P g s.

LaTeX

$$G.LocalInvariantProp G' P → (∀ y ∈ s, g' y = g y) → LiftPropOn P g' s ↔ LiftPropOn P g s$$

Lean4

theorem liftPropAt_of_mem_maximalAtlas [HasGroupoid M G] (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y)
    (he : e ∈ maximalAtlas M G) (hx : x ∈ e.source) : LiftPropAt Q e x :=
  by
  simp_rw [LiftPropAt, hG.liftPropWithinAt_indep_chart he hx G.id_mem_maximalAtlas (mem_univ _),
    (e.continuousAt hx).continuousWithinAt, true_and]
  exact hG.congr' (e.eventually_right_inverse' hx) (hQ _)

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