liftPropWithinAt_of_liftPropAt_of_mem_nhds

English

A variant of congruence with nhdsWithin and equation of germs.

Русский

Вариант конгруэнтности с nhdsWithin и жермовыми равенствами.

LaTeX

$$$\mathrm{LiftPropWithinAt}(P,g,s,x) \leftrightarrow \mathrm{LiftPropWithinAt}(P,g',s,x) \text{ under appropriate EventuallyEq conditions.}$$$

Lean4

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

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