## Stream: maths

### Topic: unique limit

#### 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
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)

#### 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' _ _ _