Theorem: Super.isOpen_post (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
inst✝ : OnePreimage s
⊢ IsOpen s.post
Tactic:
set f := fun x : ℂ × S ↦ s.p x.1 - s.potential x.1 x.2
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
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
⊢ IsOpen s.post

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
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
⊢ IsOpen s.post
Tactic:
have fc : LowerSemicontinuous f :=
  (s.lowerSemicontinuous_p.comp continuous_fst).add
    (Continuous.potential s).neg.lowerSemicontinuous
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
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
⊢ IsOpen s.post

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
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
⊢ IsOpen s.post
Tactic:
have e : s.post = f ⁻¹' Ioi 0 :=
  Set.ext fun _ ↦ by
    simp only [Super.post, mem_setOf, Postcritical, mem_preimage, mem_Ioi, sub_pos, f]
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
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
e : s.post = f ⁻¹' Ioi 0
⊢ IsOpen s.post

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
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
e : s.post = f ⁻¹' Ioi 0
⊢ IsOpen s.post
Tactic:
rw [e]
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
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
e : s.post = f ⁻¹' Ioi 0
⊢ IsOpen (f ⁻¹' Ioi 0)

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
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
e : s.post = f ⁻¹' Ioi 0
⊢ IsOpen (f ⁻¹' Ioi 0)
Tactic:
exact fc.isOpen_preimage _
State after:
no goals

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
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
x✝ : ℂ × S
⊢ x✝ ∈ s.post ↔ x✝ ∈ f ⁻¹' Ioi 0
Tactic:
simp only [Super.post, mem_setOf, Postcritical, mem_preimage, mem_Ioi, sub_pos, f]
State after:
no goals