Theorem: Super.continuous_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
n : ℕ
gc : Continuous g
hc : Continuous h
⊢ Continuous fun x => (f (g x))^[n] (h 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
gc : Continuous g
hc : Continuous h
⊢ Continuous fun x => (f (g x))^[0] (h 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
gc : Continuous g
hc : Continuous h✝
n : ℕ
h : Continuous fun x => (f (g x))^[n] (h✝ x)
⊢ Continuous fun x => (f (g x))^[n + 1] (h✝ 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
gc : Continuous g
hc : Continuous h
⊢ Continuous fun x => (f (g x))^[0] (h 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
gc : Continuous g
hc : Continuous h✝
n : ℕ
h : Continuous fun x => (f (g x))^[n] (h✝ x)
⊢ Continuous fun x => (f (g x))^[n + 1] (h✝ 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
gc : Continuous g
hc : Continuous h
⊢ Continuous fun x => h 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
gc : Continuous g
hc : Continuous h✝
n : ℕ
h : Continuous fun x => (f (g x))^[n] (h✝ x)
⊢ Continuous fun x => (f (g x))^[n + 1] (h✝ 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
gc : Continuous g
hc : Continuous h
⊢ Continuous fun x => h 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
gc : Continuous g
hc : Continuous h✝
n : ℕ
h : Continuous fun x => (f (g x))^[n] (h✝ x)
⊢ Continuous fun x => (f (g x))^[n + 1] (h✝ 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
gc : Continuous g
hc : Continuous h✝
n : ℕ
h : Continuous fun x => (f (g x))^[n] (h✝ x)
⊢ Continuous fun x => (f (g x))^[n + 1] (h✝ 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
gc : Continuous g
hc : Continuous h✝
n : ℕ
h : Continuous fun x => (f (g x))^[n] (h✝ x)
⊢ Continuous fun x => (f (g x))^[n + 1] (h✝ 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
gc : Continuous g
hc : Continuous h✝
n : ℕ
h : Continuous fun x => (f (g x))^[n] (h✝ x)
⊢ Continuous fun x => (f (g x) ∘ (f (g x))^[n]) (h✝ 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
gc : Continuous g
hc : Continuous h✝
n : ℕ
h : Continuous fun x => (f (g x))^[n] (h✝ x)
⊢ Continuous fun x => (f (g x) ∘ (f (g x))^[n]) (h✝ x)
Tactic:
exact s.fa.continuous.comp (gc.prod_mk h)
State after:
no goals