Theorem: Super.isOpen_ext (Ray/Dynamics/Ray.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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ IsOpen s.ext
Tactic:
set f := fun y : ℂ × ℂ ↦ s.p y.1 - abs y.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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
⊢ IsOpen s.ext

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
⊢ IsOpen s.ext
Tactic:
have fc : LowerSemicontinuous f :=
  (s.lowerSemicontinuous_p.comp continuous_fst).add
    (Complex.continuous_abs.comp continuous_snd).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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
⊢ IsOpen s.ext

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
⊢ IsOpen s.ext
Tactic:
have e : s.ext = f ⁻¹' Ioi 0 :=
  Set.ext fun _ ↦ by simp only [Super.ext, mem_setOf, 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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
e : s.ext = f ⁻¹' Ioi 0
⊢ IsOpen s.ext

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
e : s.ext = f ⁻¹' Ioi 0
⊢ IsOpen s.ext
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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
e : s.ext = 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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
e : s.ext = 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 x : ℂ
a z : S
d n : ℕ
s✝ : Super f✝ d a
y : ℂ × ℂ
s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × ℂ → ℝ := fun y => s.p y.1 - Complex.abs y.2
fc : LowerSemicontinuous f
x✝ : ℂ × ℂ
⊢ x✝ ∈ s.ext ↔ x✝ ∈ f ⁻¹' Ioi 0
Tactic:
simp only [Super.ext, mem_setOf, mem_preimage, mem_Ioi, sub_pos, f]
State after:
no goals