Theorem: Super.potential_lt_one_iff (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
⊢ s.potential c z < 1 ↔ ∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
refine ⟨?_, s.potential_lt_one⟩
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
⊢ s.potential c z < 1 → ∃ n, (c, (f c)^[n] z) ∈ s.near

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
⊢ s.potential c z < 1 → ∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
intro h
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
h : s.potential c z < 1
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near

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
h : s.potential c z < 1
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
contrapose h
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
h : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ¬s.potential c z < 1

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
h : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ¬s.potential c z < 1
Tactic:
simp only [not_exists] at h
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
h : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ ¬s.potential c z < 1

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
h : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ ¬s.potential c z < 1
Tactic:
simp only [s.potential_eq_one h, lt_self_iff_false, not_false_iff]
State after:
no goals