E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∀ (u : ℕ → (n : ℕ) → E n),
    (∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N) → ∃ x, Tendsto u atTop (𝓝 x)
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ CompleteSpace ((n : ℕ) → E n)
refine' Metric.complete_of_convergent_controlled_sequences (fun n => (1 / 2) ^ n) (by simp) _
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N
⊢ ∃ x, Tendsto u atTop (𝓝 x)
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∀ (u : ℕ → (n : ℕ) → E n),
    (∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N) → ∃ x, Tendsto u atTop (𝓝 x)
intro u hu
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N
i : ℕ
⊢ Tendsto (fun i_1 => u i_1 i) atTop (𝓝 (u i i))
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N
⊢ ∃ x, Tendsto u atTop (𝓝 x)
refine' ⟨fun n => u n n, tendsto_pi_nhds.2 fun i => _⟩
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N
i : ℕ
⊢ (fun x => u i i) =ᶠ[atTop] fun i_1 => u i_1 i
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N
i : ℕ
⊢ Tendsto (fun i_1 => u i_1 i) atTop (𝓝 (u i i))
refine' tendsto_const_nhds.congr' _
case h
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N
i n : ℕ
hn : n ∈ Ici i
⊢ u i i = u n i
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N
i : ℕ
⊢ (fun x => u i i) =ᶠ[atTop] fun i_1 => u i_1 i
filter_upwards [Filter.Ici_mem_atTop i]with n hn
no goals
case h
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
u : ℕ → (n : ℕ) → E n
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N
i n : ℕ
hn : n ∈ Ici i
⊢ u i i = u n i
exact apply_eq_of_dist_lt (hu i i n le_rfl hn) le_rfl
no goals
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
⊢ ∀ (n : ℕ), 0 < (fun n => (1 / 2) ^ n) n
simp