Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC