Theorem: Super.continuousOn_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
t : Set T
n : ℕ
gc : ContinuousOn g t
hc : ContinuousOn h t
⊢ ContinuousOn (fun x => (f (g x))^[n] (h x)) t
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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h t
⊢ ContinuousOn (fun x => (f (g x))^[0] (h x)) t

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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x))^[n + 1] (h✝ x)) t

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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h t
⊢ ContinuousOn (fun x => (f (g x))^[0] (h x)) t

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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x))^[n + 1] (h✝ x)) t
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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h t
⊢ ContinuousOn (fun x => h x) t

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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x))^[n + 1] (h✝ x)) t

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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h t
⊢ ContinuousOn (fun x => h x) t

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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x))^[n + 1] (h✝ x)) t
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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x))^[n + 1] (h✝ x)) t

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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x))^[n + 1] (h✝ x)) t
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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x) ∘ (f (g x))^[n]) (h✝ x)) t

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
t : Set T
gc : ContinuousOn g t
hc : ContinuousOn h✝ t
n : ℕ
h : ContinuousOn (fun x => (f (g x))^[n] (h✝ x)) t
⊢ ContinuousOn (fun x => (f (g x) ∘ (f (g x))^[n]) (h✝ x)) t
Tactic:
exact s.fa.continuous.comp_continuousOn (gc.prod h)
State after:
no goals