liftPropAt_of_liftPropWithinAt — Mathlib

English

If g' ≈ g near x in nhdsWithin g, then LiftPropWithinAt across g' equals LiftPropWithinAt across g.

Русский

Если g' совпадает с g локально возле x в nhdsWithin, то LiftPropWithinAt совпадает.

LaTeX

$$$\mathrm{LiftPropWithinAt}(P,g,s,x) \rightarrow \mathrm{nhdsWithin\ x}(s).\EventuallyEq g' g \rightarrow g'(x)=g(x) \rightarrow \mathrm{LiftPropWithinAt}(P,g',s,x).$$$

Lean4

theorem liftPropAt_of_liftPropWithinAt (h : LiftPropWithinAt P g s x) (hs : s ∈ 𝓝 x) : LiftPropAt P g x := by
  rwa [← univ_inter s, hG.liftPropWithinAt_inter hs] at h

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