liftPropAt_congr_of_eventuallyEq — Mathlib

English

Let G be a LocalInvariantProp. Then LiftPropAt P g' x iff LiftPropAt P g x whenever g' =ᶠ_{𝓝 x} g.

Русский

Пусть G имеет локальную инвариантность. Тогда LiftPropAt P g' x эквивалентно LiftPropAt P g x, если g' =·_{𝓝 x} g.

LaTeX

$$$G.LocalInvariantProp\ G' P \to (g' =^{\cdot}_{\mathcal{N} x} g) \to LiftPropAt\ P\ g'\ x \leftrightarrow LiftPropAt\ P\ g\ x$$

Lean4

theorem liftPropAt_congr_of_eventuallyEq (h : LiftPropAt P g x) (h₁ : g' =ᶠ[𝓝 x] g) : LiftPropAt P g' x :=
  (hG.liftPropAt_congr_iff_of_eventuallyEq h₁).mpr h

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