Zulip Chat Archive

Stream: maths

Topic: unique limit


view this post on Zulip Patrick Massot (Jan 19 2019 at 22:20):

@Kevin Buzzard I looked at https://github.com/ImperialCollegeLondon/M1P1-lean/blob/master/src/limits.lean There is a comment saying you don't know how to use wlog. I think what you were looking for is:

lemma limits_aux (a :   ) (l m : ) (hl : is_limit a l)
(hm : is_limit a m) : l = m :=
begin
  by_contradiction h,
  wlog h' : l < m,
  { have := lt_trichotomy l m, tauto, },

and then put the proof exactly as it was (and remove "_aux" from the name of the lemma since it's now directly proving what you want)

view this post on Zulip Patrick Massot (Jan 19 2019 at 22:22):

But your proof is rather contrived. Why not doing:

lemma zero_of_abs_lt_all (x : ) (h :  ε, ε > 0  |x| < ε) : x = 0 :=
eq_zero_of_abs_eq_zero $ eq_of_le_of_forall_le_of_dense (abs_nonneg x) $ λ ε ε_pos, le_of_lt (h ε ε_pos)

theorem limits_are_unique (a :   ) (l m : ) (hl : is_limit a l)
(hm : is_limit a m) : l = m :=
begin
  suffices :  ε : , ε > 0  |l - m| < ε,
  from eq_of_sub_eq_zero (zero_of_abs_lt_all _ this),
  intros ε ε_pos,
  cases hl (ε/2) (by linarith) with Nl H,
  cases hm (ε/2) (by linarith) with Nm H',
  let N := max Nl Nm,
  specialize H  N (le_max_left  _ _),
  specialize H' N (le_max_right _ _),
  exact calc |l - m|  |a N - m| + |a N - l| : triangle' _ _ _
   ... < ε/2 + ε/2 : add_lt_add H' H
   ... = ε : by ring,
end

which seems to obey your stylistic constraints?


Last updated: May 11 2021 at 16:22 UTC