no goals
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
X : Type ?u.8629
inst✝⁶ : TopologicalSpace H
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : TopologicalSpace X
P : (H → H') → Set H → H → Prop
f : M → M'
x : M
⊢ LiftPropAt P f x ↔
    ContinuousAt f x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(LocalHomeomorph.symm (chartAt H x))) univ (↑(chartAt H x) x)
rw [LiftPropAt, LiftPropWithinAt, continuousWithinAt_univ, preimage_univ]