Theorem: Super.mem_ps (Ray/Dynamics/Postcritical.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
c : ℂ
inst✝ : OnePreimage s
⊢ s.p c ∈ s.ps c
Tactic:
rw [← s.compact_ps.isClosed.closure_eq]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
c : ℂ
inst✝ : OnePreimage s
⊢ s.p c ∈ closure (s.ps c)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
c : ℂ
inst✝ : OnePreimage s
⊢ s.p c ∈ closure (s.ps c)
Tactic:
exact csInf_mem_closure s.nonempty_ps s.bddBelow_ps
State after:
no goals