Theorem: Super.continuousAt_iter (Ray/Dynamics/BottcherNearM.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 : S
d n✝ : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h : T → S
x : T
n : ℕ
gc : ContinuousAt g x
hc : ContinuousAt h x
⊢ ContinuousAt (fun x => (f (g x))^[n] (h x)) x
Tactic:
induction' n with n h
State after:
case zero
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h x
⊢ ContinuousAt (fun x => (f (g x))^[0] (h x)) x

case succ
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h✝ : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x))^[n + 1] (h✝ x)) x

State before:
case zero
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h x
⊢ ContinuousAt (fun x => (f (g x))^[0] (h x)) x

case succ
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h✝ : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x))^[n + 1] (h✝ x)) x
Tactic:
simp only [Function.iterate_zero, id]
State after:
case zero
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h x
⊢ ContinuousAt (fun x => h x) x

case succ
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h✝ : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x))^[n + 1] (h✝ x)) x

State before:
case zero
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h x
⊢ ContinuousAt (fun x => h x) x

case succ
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h✝ : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x))^[n + 1] (h✝ x)) x
Tactic:
exact hc
State after:
case succ
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h✝ : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x))^[n + 1] (h✝ x)) x

State before:
case succ
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h✝ : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x))^[n + 1] (h✝ x)) x
Tactic:
simp_rw [Function.iterate_succ']
State after:
case succ
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h✝ : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x) ∘ (f (g x))^[n]) (h✝ x)) x

State before:
case succ
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
T : Type
inst✝ : TopologicalSpace T
g : T → ℂ
h✝ : T → S
x : T
gc : ContinuousAt g x
hc : ContinuousAt h✝ x
n : ℕ
h : ContinuousAt (fun x => (f (g x))^[n] (h✝ x)) x
⊢ ContinuousAt (fun x => (f (g x) ∘ (f (g x))^[n]) (h✝ x)) x
Tactic:
exact (s.fa _).continuousAt.comp (gc.prod h)
State after:
no goals