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: May 14 2021 at 12:18 UTC