internlm/Lean-Github huggingface dataset:
Theorem: Barrier.potential_large
Proof state before:
case h.right
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
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e✝ : ℂ
z✝ : S
ps : (e✝, z✝) ∈ t
pm : IsMinOn (uncurry s.potential) t (e✝, z✝)
e : ℂ
z : S
m : (e, z) ∈ t
⊢ s.potential e✝ z✝ ≤ s.potential e z
Tactic:
simp only [isMinOn_iff, uncurry] at pm ⊢
Proof state after:
case h.right
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
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e✝ : ℂ
z✝ : S
ps : (e✝, z✝) ∈ t
e : ℂ
z : S
m : (e, z) ∈ t
pm : ∀ x ∈ t, s.potential e✝ z✝ ≤ s.potential x.1 x.2
⊢ s.potential e✝ z✝ ≤ s.potential e z
Theorem: Barrier.potential_large
Proof state before:
case h.right
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
inst✝ : OnePreimage s
n t : Set (ℂ × S)
b : Barrier s c n t
t0 : t.Nonempty
pc : ContinuousOn (uncurry s.potential) t
e✝ : ℂ
z✝ : S
ps : (e✝, z✝) ∈ t
e : ℂ
z : S
m : (e, z) ∈ t
pm : ∀ x ∈ t, s.potential e✝ z✝ ≤ s.potential x.1 x.2
⊢ s.potential e✝ z✝ ≤ s.potential e z
Tactic:
exact pm _ m
Proof state after:
no goals
Theorem: Barrier.closed_fast
Proof 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
Proof 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)
Theorem: Barrier.closed_fast
Proof 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
Proof 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)
Theorem: Barrier.closed_fast
Proof 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
Proof 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)
Theorem: Barrier.closed_fast
Proof 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
Proof 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
Theorem: Barrier.closed_fast
Proof 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
Proof 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
Theorem: Barrier.closed_fast
Proof 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
Proof 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
Theorem: Barrier.closed_fast
Proof 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
Proof 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
Theorem: Barrier.closed_fast
Proof 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]
Proof 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
Theorem: Barrier.closed_fast
Proof 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
Proof 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
Theorem: Barrier.closed_fast
Proof 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']
Proof 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)
Theorem: Barrier.closed_fast
Proof 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)
Proof state after:
no goals
Theorem: Barrier.mem_fast
Proof 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 : ℕ
e : ℂ
z : S
⊢ (e, z) ∈ b.fast m ↔ ∃ n < m, (e, (f e)^[n] z) ∈ t
Tactic:
simp only [Barrier.fast, Set.mem_iUnion, Set.mem_preimage]
Proof state after:
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 : ℕ
e : ℂ
z : S
⊢ (∃ i, (e, (f e)^[↑i] z) ∈ t) ↔ ∃ n < m, (e, (f e)^[n] z) ∈ t
Theorem: Barrier.mem_fast
Proof 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 : ℕ
e : ℂ
z : S
⊢ (∃ i, (e, (f e)^[↑i] z) ∈ t) ↔ ∃ n < m, (e, (f e)^[n] z) ∈ t
Tactic:
constructor
Proof state after:
case mp
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 : ℕ
e : ℂ
z : S
⊢ (∃ i, (e, (f e)^[↑i] z) ∈ t) → ∃ n < m, (e, (f e)^[n] z) ∈ t

case mpr
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 : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t
Theorem: Barrier.mem_fast
Proof state before:
case mp
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 : ℕ
e : ℂ
z : S
⊢ (∃ i, (e, (f e)^[↑i] z) ∈ t) → ∃ n < m, (e, (f e)^[n] z) ∈ t

case mpr
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 : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t
Tactic:
intro h
Proof state after:
case mp
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 : ℕ
e : ℂ
z : S
h : ∃ i, (e, (f e)^[↑i] z) ∈ t
⊢ ∃ n < m, (e, (f e)^[n] z) ∈ t

case mpr
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 : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t
Theorem: Barrier.mem_fast
Proof state before:
case mp
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 : ℕ
e : ℂ
z : S
h : ∃ i, (e, (f e)^[↑i] z) ∈ t
⊢ ∃ n < m, (e, (f e)^[n] z) ∈ t

case mpr
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 : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t
Tactic:
rcases h with ⟨n, h⟩
Proof state after:
case mp.intro
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 : ℕ
e : ℂ
z : S
n : Fin m
h : (e, (f e)^[↑n] z) ∈ t
⊢ ∃ n < m, (e, (f e)^[n] z) ∈ t

case mpr
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 : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t
Theorem: Barrier.mem_fast
Proof state before:
case mp.intro
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 : ℕ
e : ℂ
z : S
n : Fin m
h : (e, (f e)^[↑n] z) ∈ t
⊢ ∃ n < m, (e, (f e)^[n] z) ∈ t

case mpr
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 : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t
Tactic:
use n, Fin.is_lt _, h
Proof state after:
case mpr
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 : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t
Theorem: Barrier.mem_fast
Proof state before:
case mpr
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 : ℕ
e : ℂ
z : S
⊢ (∃ n < m, (e, (f e)^[n] z) ∈ t) → ∃ i, (e, (f e)^[↑i] z) ∈ t
Tactic:
intro h
Proof state after:
case mpr
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 : ℕ
e : ℂ
z : S
h : ∃ n < m, (e, (f e)^[n] z) ∈ t
⊢ ∃ i, (e, (f e)^[↑i] z) ∈ t
Theorem: Barrier.mem_fast
Proof state before:
case mpr
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 : ℕ
e : ℂ
z : S
h : ∃ n < m, (e, (f e)^[n] z) ∈ t
⊢ ∃ i, (e, (f e)^[↑i] z) ∈ t
Tactic:
rcases h with ⟨n, nm, h⟩
Proof state after:
case mpr.intro.intro
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 : ℕ
e : ℂ
z : S
n : ℕ
nm : n < m
h : (e, (f e)^[n] z) ∈ t
⊢ ∃ i, (e, (f e)^[↑i] z) ∈ t
Theorem: Barrier.mem_fast
Proof state before:
case mpr.intro.intro
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 : ℕ
e : ℂ
z : S
n : ℕ
nm : n < m
h : (e, (f e)^[n] z) ∈ t
⊢ ∃ i, (e, (f e)^[↑i] z) ∈ t
Tactic:
use⟨n, nm⟩, h
Proof state after:
no goals
Theorem: Barrier.fast_reaches
Proof 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 : ℕ
e : ℂ
z : S
q : (e, z) ∈ b.fast m
⊢ ∃ n, (e, (f e)^[n] z) ∈ s.near
Tactic:
rw [b.mem_fast] at q
Proof state after:
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 : ℕ
e : ℂ
z : S
q : ∃ n < m, (e, (f e)^[n] z) ∈ t
⊢ ∃ n, (e, (f e)^[n] z) ∈ s.near
Theorem: Barrier.fast_reaches
Proof 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 : ℕ
e : ℂ
z : S
q : ∃ n < m, (e, (f e)^[n] z) ∈ t
⊢ ∃ n, (e, (f e)^[n] z) ∈ s.near
Tactic:
rcases q with ⟨n, _, q⟩
Proof state after:
case intro.intro
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 : ℕ
e : ℂ
z : S
n : ℕ
left✝ : n < m
q : (e, (f e)^[n] z) ∈ t
⊢ ∃ n, (e, (f e)^[n] z) ∈ s.near
Theorem: Barrier.fast_reaches
Proof state before:
case intro.intro
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 : ℕ
e : ℂ
z : S
n : ℕ
left✝ : n < m
q : (e, (f e)^[n] z) ∈ t
⊢ ∃ n, (e, (f e)^[n] z) ∈ s.near
Tactic:
exact ⟨n, b.near q⟩
Proof state after:
no goals
Theorem: Continuous.potential
Proof 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
inst✝ : OnePreimage s
⊢ Continuous (uncurry s.potential)
Tactic:
refine continuous_iff_lower_upperSemicontinuous.mpr ⟨?_, UpperSemicontinuous.potential s⟩
Proof state after:
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
inst✝ : OnePreimage s
⊢ LowerSemicontinuous (uncurry s.potential)
Theorem: Continuous.potential
Proof 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
inst✝ : OnePreimage s
⊢ LowerSemicontinuous (uncurry s.potential)
Tactic:
intro ⟨c, z⟩
Proof state after:
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
inst✝ : OnePreimage s
c : ℂ
z : S
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)
Theorem: Continuous.potential
Proof 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
inst✝ : OnePreimage s
c : ℂ
z : S
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
by_cases re : ∃ n, (c, (f c)^[n] z) ∈ s.near
Proof state after:
case pos
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
inst✝ : OnePreimage s
c : ℂ
z : S
re : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)

case neg
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
inst✝ : OnePreimage s
c : ℂ
z : S
re : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)
Theorem: Continuous.potential
Proof state before:
case pos
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
inst✝ : OnePreimage s
c : ℂ
z : S
re : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)

case neg
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
inst✝ : OnePreimage s
c : ℂ
z : S
re : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
exact (ContinuousAt.potential_of_reaches s re).lowerSemicontinuousAt
Proof state after:
case neg
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
inst✝ : OnePreimage s
c : ℂ
z : S
re : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)
Theorem: Continuous.potential
Proof state before:
case neg
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
inst✝ : OnePreimage s
c : ℂ
z : S
re : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
simp only [not_exists] at re
Proof state after:
case neg
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
inst✝ : OnePreimage s
c : ℂ
z : S
re : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ LowerSemicontinuousAt (uncurry s.potential) (c, z)