liftPropWithinAt_inter — Mathlib

English

If two germ expressions agree in the neighborhood of a point up to eventual equality, then LiftPropWithinAt respects this equivalence.

Русский

Если выражения жерма совпадают в окрестности точки вплоть до конца, то LiftPropWithinAt сохраняет эту эквивалентность.

LaTeX

$$$(\text{nhdsWithin } x)\text{ EventuallyEq } s t \implies \text{LiftPropWithinAt}(P,g,s,x)\;\Leftrightarrow\; \text{LiftPropWithinAt}(P,g,t,x).$$$

Lean4

theorem liftPropWithinAt_inter (ht : t ∈ 𝓝 x) : LiftPropWithinAt P g (s ∩ t) x ↔ LiftPropWithinAt P g s x :=
  hG.liftPropWithinAt_inter' (mem_nhdsWithin_of_mem_nhds ht)

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