Zulip Chat Archive

Stream: new members

Topic: closeness


Iocta (Jul 13 2020 at 04:39):

example (a b c ε  : real) :
ε > 0  | a - c |  ε  | b - c |  ε  | a - b |  2 * ε :=
sorry

Is there some lemma like this?

Scott Morrison (Jul 13 2020 at 04:55):

I doubt you'll find that "out of the box" in the sense that library_search can solve it.

Scott Morrison (Jul 13 2020 at 04:56):

but the result with two different epsilons is hopefully findable by library_search

Iocta (Jul 13 2020 at 05:49):

I don't see it

example (a b c ε ε'   : real) :
ε > 0
 ε' > 0
 | a - c |  ε
 | b - c |  ε'
 | a - b |  ε + ε'  :=
begin
intros e_pos e'_pos hac hbc,
library_search, -- doesn't find it
end

Shing Tak Lam (Jul 13 2020 at 06:05):

I think linarith might be what you're looking for?

import data.real.basic

notation `|` x `|` := abs x

example (a b c ε ε' : real) :
ε > 0
 ε' > 0
 | a - c |  ε
 | b - c |  ε'
 | a - b |  ε + ε'  :=
begin
intros e_pos e'_pos hac hbc,
rw abs_le at *,
split;
  linarith
end

Last updated: Dec 20 2023 at 11:08 UTC