Theorem: Barrier.closed_fast (Ray/Dynamics/Potential.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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
⊢ IsClosed (b.fast m)
Tactic:
apply isClosed_iUnion_of_finite
State after:
case h
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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
⊢ ∀ (i : Fin m), IsClosed ((fun p => (p.1, (f p.1)^[↑i] p.2)) ⁻¹' t)

State before:
case h
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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
⊢ ∀ (i : Fin m), IsClosed ((fun p => (p.1, (f p.1)^[↑i] p.2)) ⁻¹' t)
Tactic:
intro k
State after:
case h
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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
k : Fin m
⊢ IsClosed ((fun p => (p.1, (f p.1)^[↑k] p.2)) ⁻¹' t)

State before:
case h
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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
k : Fin m
⊢ IsClosed ((fun p => (p.1, (f p.1)^[↑k] p.2)) ⁻¹' t)
Tactic:
refine IsClosed.preimage ?_ b.compact.isClosed
State after:
case h
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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
k : Fin m
⊢ Continuous fun p => (p.1, (f p.1)^[↑k] p.2)

State before:
case h
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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
k : Fin m
⊢ Continuous fun p => (p.1, (f p.1)^[↑k] p.2)
Tactic:
apply continuous_fst.prod_mk
State after:
case h
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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
k : Fin m
⊢ Continuous fun x => (f x.1)^[↑k] x.2

State before:
case h
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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
k : Fin m
⊢ Continuous fun x => (f x.1)^[↑k] x.2
Tactic:
generalize hn : (k : ℕ) = n
State after:
case h
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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m : ℕ
k : Fin m
n : ℕ
hn : ↑k = n
⊢ Continuous fun x => (f x.1)^[n] x.2

State before:
case h
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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m : ℕ
k : Fin m
n : ℕ
hn : ↑k = n
⊢ Continuous fun x => (f x.1)^[n] x.2
Tactic:
clear k hn
State after:
case h
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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m n : ℕ
⊢ Continuous fun x => (f x.1)^[n] x.2

State before:
case h
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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m n : ℕ
⊢ Continuous fun x => (f x.1)^[n] x.2
Tactic:
induction' n with n h
State after:
case h.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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
⊢ Continuous fun x => (f x.1)^[0] x.2

case h.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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m n : ℕ
h : Continuous fun x => (f x.1)^[n] x.2
⊢ Continuous fun x => (f x.1)^[n + 1] x.2

State before:
case h.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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
⊢ Continuous fun x => (f x.1)^[0] x.2

case h.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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m n : ℕ
h : Continuous fun x => (f x.1)^[n] x.2
⊢ Continuous fun x => (f x.1)^[n + 1] x.2
Tactic:
simp only [Function.iterate_zero_apply]
State after:
case h.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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
⊢ Continuous fun x => x.2

case h.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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m n : ℕ
h : Continuous fun x => (f x.1)^[n] x.2
⊢ Continuous fun x => (f x.1)^[n + 1] x.2

State before:
case h.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
n t : Set (ℂ × S)
b : Barrier s c n t
m : ℕ
⊢ Continuous fun x => x.2

case h.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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m n : ℕ
h : Continuous fun x => (f x.1)^[n] x.2
⊢ Continuous fun x => (f x.1)^[n + 1] x.2
Tactic:
exact continuous_snd
State after:
case h.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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m n : ℕ
h : Continuous fun x => (f x.1)^[n] x.2
⊢ Continuous fun x => (f x.1)^[n + 1] x.2

State before:
case h.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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m n : ℕ
h : Continuous fun x => (f x.1)^[n] x.2
⊢ Continuous fun x => (f x.1)^[n + 1] x.2
Tactic:
simp only [Function.iterate_succ_apply']
State after:
case h.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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m n : ℕ
h : Continuous fun x => (f x.1)^[n] x.2
⊢ Continuous fun x => f x.1 ((f x.1)^[n] x.2)

State before:
case h.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
n✝ t : Set (ℂ × S)
b : Barrier s c n✝ t
m n : ℕ
h : Continuous fun x => (f x.1)^[n] x.2
⊢ Continuous fun x => f x.1 ((f x.1)^[n] x.2)
Tactic:
exact s.fa.continuous.comp (continuous_fst.prod_mk h)
State after:
no goals