## Stream: general

### Topic: Simplify dist def for sequence_tendsto

#### ZHAO Jinxiang (Aug 27 2022 at 14:20):

import data.real.basic
import topology.metric_space.basic

def sequence_tendsto (a : ℕ → ℝ) (t : ℝ) :=
∀ ε > 0, ∃ N , ∀ n, N ≤ n → |a n - t| < ε

def sequence_tendsto₁ (a : ℕ → ℝ) (t : ℝ) :=
∀ ε > 0, ∃ N , ∀ n, N ≤ n → dist t (a n) < ε
example : sequence_tendsto = sequence_tendsto₁ := begin
ext a t,
unfold sequence_tendsto sequence_tendsto₁ dist,
-- Help me here: code below are too redundant
split,
{
intros h a b,
specialize h a b,
cases h with N h,
use N,
intros n hn,
specialize h n hn,
rw <-abs_neg,
simp,
assumption,
},
{
intros h a b,
specialize h a b,
cases h with N h,
use N,
intros n hn,
specialize h n hn,
rw <-abs_neg,
simp,
assumption,
}
end


code are too redundant, can you simplify it?

#### FR (Aug 27 2022 at 14:33):

import data.real.basic
import topology.metric_space.basic

def sequence_tendsto (a : ℕ → ℝ) (t : ℝ) :=
∀ ε > 0, ∃ N, ∀ n, N ≤ n → |a n - t| < ε

def sequence_tendsto₁ (a : ℕ → ℝ) (t : ℝ) :=
∀ ε > 0, ∃ N, ∀ n, N ≤ n → dist t (a n) < ε

example : sequence_tendsto = sequence_tendsto₁ :=
begin
ext a t,
unfold sequence_tendsto sequence_tendsto₁ dist,
simp_rw abs_sub_comm,
end


Last updated: Aug 03 2023 at 10:10 UTC