liftPropWithinAt_inter' — Mathlib

English

If a germ-invariant property holds for two charts, then lift properties agree after composition with these charts.

Русский

Если жерменно-инвариантное свойство верно для двух чартов, то свойства подъёма согласуются после композиции с чартами.

LaTeX

$$$P(f\!\circ\! g\!\circ\! e^{-1})(s)(x) \iff P(f'\!\circ\! g\!\circ\! e'^{-1})(s)(x).$$$

Lean4

theorem liftPropWithinAt_inter' (ht : t ∈ 𝓝[s] x) : LiftPropWithinAt P g (s ∩ t) x ↔ LiftPropWithinAt P g s x :=
  by
  rw [liftPropWithinAt_iff', liftPropWithinAt_iff', continuousWithinAt_inter' ht, hG.congr_set]
  simp_rw [eventuallyEq_set, mem_preimage,
    (chartAt _ x).eventually_nhds' (fun x ↦ x ∈ s ∩ t ↔ x ∈ s) (mem_chart_source _ x)]
  exact (mem_nhdsWithin_iff_eventuallyEq.mp ht).symm.mem_iff

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