liftPropWithinAt_congr_of_eventuallyEq_of_mem

English

Let G and G' be structure groupoids with a Local Invariant Property P. If a local lift PropWithinAt holds for g on a set s around x, and g' agrees with g on the nhdsWithin of x relative to s, and x lies in s, then LiftPropWithinAt P g' s x also holds.

Русский

Пусть G и G' — структуры группоидов с локальным инвариантным свойством P. Если для отображения g на множестве s в окрестности x выполняется свойство LiftPropWithinAt, и g совпадает с g' на окрестности x внутри s, и x ∈ s, тогда верно LiftPropWithinAt P g' s x.

LaTeX

$$$G.Loc\alInvariantProp G' P \;\to\; (\text{LiftPropWithinAt } P\ g\ s\ x) \to (\, (nhdsWithin\ x\ s) .EventuallyEq\ g'\ g\,) \to x \in s \;\to\; \text{LiftPropWithinAt } P\ g'\ s\ x$$

Lean4

theorem liftPropWithinAt_congr_of_eventuallyEq_of_mem (h : LiftPropWithinAt P g s x) (h₁ : g' =ᶠ[𝓝[s] x] g)
    (h₂ : x ∈ s) : LiftPropWithinAt P g' s x :=
  liftPropWithinAt_congr_of_eventuallyEq hG h h₁ (mem_of_mem_nhdsWithin h₂ h₁ :)

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