closeness

Stream: new members

[Iocta]

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

Is there some lemma like this?

[Scott Morrison]

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

[Scott Morrison]

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

[Iocta]

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]

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