# Zulip Chat Archive

## Stream: new members

### Topic: Proving triangle inequality

#### ambiso (Feb 22 2023 at 13:36):

Hi,

I'm trying to prove a relatively simple inequality (that I hope to be true), and on the path to that I want to prove the triangle theorem.

Unfortunately, I'm kind of lost what tactics or existing theorems to use to help me get there.

This is the final theorem I want to prove:

```
theorem my_ineq (a b u t: ℚ) : (0≤a ∧ a≤1 ∧ 0≤b ∧ b≤1 ∧ 0≤u ∧ u≤1 ∧ 1≤t ∧ u≤a ∧ a≤t*u) → |a-b| ≤ |u-b| + (t-1)*u := by sorry
```

I currently have:

```
import data.rat.basic
import data.rat.order
import algebra.abs
#check (abs_add : ∀ a b : ℚ, |a + b| ≤ |a| + |b|)
theorem triangle_ineq (a b c : ℚ) : |a-b| ≤ |a-c| + |c-b| := by sorry
```

Can I use the abs_add proposition(?) to help me in the proof? Why does it not require any explicit proof for the #check?

I'd appreciate any help or pointers to relevant material that I can use.

I've completed parts of https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/, but have no experience in handling rationals. I was hoping the existing theorems could help me, but I failed to find e.g. the triangle inequality.

#### Notification Bot (Feb 22 2023 at 13:39):

This topic was moved here from #general > Proving triangle inequality by Eric Wieser.

#### Eric Wieser (Feb 22 2023 at 13:40):

Can I use the abs_add proposition(?) to help me in the proof?

Yes, definitely! What values do you want to use for `a`

and `b`

?

Why does it not require any explicit proof for the #check?

You gave the explicit proof, it was `abs_add`

!

#### Eric Wieser (Feb 22 2023 at 13:41):

Perhaps this will help:

```
import data.rat.basic
import data.rat.order
import algebra.abs
theorem triangle_ineq (a b c : ℚ) : |a-b| ≤ |a-c| + |c-b| :=
begin
have : ∀ a b : ℚ, |a + b| ≤ |a| + |b| := abs_add,
-- now you have `abs_add` visible in your goal view, and can use the tactics
-- you learnt from the natural number game
sorry,
end
```

Last updated: Dec 20 2023 at 11:08 UTC