liftPropWithinAt_congr_iff — Mathlib

English

Under LocalInvariantProp, LiftPropWithinAt P g' s x is equivalent to LiftPropWithinAt P g s x when nhdsWithin x s are mutually eventually equal and x has the same image.

Русский

При локальной инвариантности LiftPropWithinAt P g' s x эквивалентно LiftPropWithinAt P g s x, если окрестности nhdsWithin x s совпадают на бесконечно малом и образ совпадает.

LaTeX

$$$G.LocalInvariantProp\ G' P \to\ (nhdsWithin\ x\ s).EventuallyEq g' g \to Eq (g'\ x) (g\ x) \to (LiftPropWithinAt\ P\ g'\ s\ x) \leftrightarrow (LiftPropWithinAt\ P\ g\ s\ x)$$

Lean4

theorem liftPropWithinAt_congr_iff (h₁ : ∀ y ∈ s, g' y = g y) (hx : g' x = g x) :
    LiftPropWithinAt P g' s x ↔ LiftPropWithinAt P g s x :=
  hG.liftPropWithinAt_congr_iff_of_eventuallyEq (eventually_nhdsWithin_of_forall h₁) hx

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