Theorem: Super.reaches_near (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✝
z : S
a : Attracts (f c) z a✝
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
Tactic:
rw [Attracts, Filter.tendsto_iff_forall_eventually_mem] at a
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ ∀ᶠ (n : ℕ) in atTop, (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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near
Tactic:
have e := a {z | (c, z) ∈ s.near} ?_
State after:
case refine_2
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
e : ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ {z | (c, z) ∈ s.near}
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near

case refine_1
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ {z | (c, z) ∈ s.near} ∈ 𝓝 a✝

State before:
case refine_2
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
e : ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ {z | (c, z) ∈ s.near}
⊢ ∀ᶠ (n : ℕ) in atTop, (c, (f c)^[n] z) ∈ s.near

case refine_1
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ {z | (c, z) ∈ s.near} ∈ 𝓝 a✝
Tactic:
exact e
State after:
case refine_1
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ {z | (c, z) ∈ s.near} ∈ 𝓝 a✝

State before:
case refine_1
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ {z | (c, z) ∈ s.near} ∈ 𝓝 a✝
Tactic:
apply IsOpen.mem_nhds
State after:
case refine_1.hs
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ IsOpen {z | (c, z) ∈ s.near}

case refine_1.hx
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ a✝ ∈ {z | (c, z) ∈ s.near}

State before:
case refine_1.hs
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ IsOpen {z | (c, z) ∈ s.near}

case refine_1.hx
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ a✝ ∈ {z | (c, z) ∈ s.near}
Tactic:
apply IsOpen.snd_preimage s.isOpen_near
State after:
case refine_1.hx
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ a✝ ∈ {z | (c, z) ∈ s.near}

State before:
case refine_1.hx
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✝
z : S
a : ∀ s ∈ 𝓝 a✝, ∀ᶠ (x : ℕ) in atTop, (f c)^[x] z ∈ s
⊢ a✝ ∈ {z | (c, z) ∈ s.near}
Tactic:
exact s.mem_near c
State after:
no goals