liftPropWithinAt_congr_of_eventuallyEq

English

If hG ensures invariance and g' ≈ g near x and g'x = g x, then LiftPropWithinAt(P,g',s,x) holds.

Русский

Если hG задаёт инвариантность и g' совпадает с g возле x, и g'x = g x, тогда LiftPropWithinAt(P,g',s,x) выполняется.

LaTeX

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

Lean4

theorem liftPropWithinAt_congr_of_eventuallyEq (h : LiftPropWithinAt P g s x) (h₁ : g' =ᶠ[𝓝[s] x] g) (hx : g' x = g x) :
    LiftPropWithinAt P g' s x := by
  refine ⟨h.1.congr_of_eventuallyEq h₁ hx, ?_⟩
  refine
    hG.congr_nhdsWithin' ?_ (by simp_rw [Function.comp_apply, (chartAt H x).left_inv (mem_chart_source H x), hx]) h.2
  simp_rw [EventuallyEq, Function.comp_apply]
  rw [(chartAt H x).eventually_nhdsWithin' (fun y ↦ chartAt H' (g' x) (g' y) = chartAt H' (g x) (g y))
      (mem_chart_source H x)]
  exact h₁.mono fun y hy ↦ by rw [hx, hy]

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