# Zulip Chat Archive

## Stream: maths

### Topic: adding negative reals

#### Joseph Corneli (Jan 28 2019 at 16:52):

After the successes with adding positive reals I thought I would try negative reals. But I'm now running into trouble. It was all looking nice up until the end.

import data.real.basic namespace negreal def negreal := {r : ℝ // r < 0} notation `ℝ₋` := negreal constants negc negd : negreal -- comparison with posreal: just supply `add_neg` instead of `add_pos` instance negreal.add : has_add negreal := ⟨λ q r,⟨q.val + r.val, add_neg q.property r.property⟩⟩ -- We will use this fact in the lemma below example : 0 < (1:ℝ) := zero_lt_one lemma neg_one_lt_zero : -1 < (0:ℝ) := begin have h0 : (0:ℝ) < 1 , from zero_lt_one, apply neg_lt_zero.mpr, -- -a < 0 ↔ 0 < a exact h0, end instance negreal.one : has_one negreal := ⟨⟨(-1:ℝ), neg_one_lt_zero⟩⟩ example : negreal := (-1:ℝ₋)

I get:

failed to synthesize type class instance for

⊢ has_neg ℝ₋

But `has_neg : Type u_1 → Type u_1`

and the usual `-`

would in fact kick me from `negreal`

to `posreal`

.

#### Kevin Buzzard (Jan 28 2019 at 16:53):

I am not sure that `has_one`

was designed to represent numbers which we would usually call `-1`

.

#### Kevin Buzzard (Jan 28 2019 at 16:55):

You have used `has_one`

, so now Lean knows what you mean by `1:R-`

#### Kevin Buzzard (Jan 28 2019 at 16:55):

(you mean -1)

#### Kevin Buzzard (Jan 28 2019 at 16:55):

but it doesn't know what you mean by `-x`

if `x`

is a `negreal`

#### Kevin Buzzard (Jan 28 2019 at 16:55):

hence the error

#### Joseph Corneli (Jan 28 2019 at 16:56):

yeah.

What's interesting (resp., annoying) is that negreal is somehow just a copy of posreal with a different paint job.

#### Kevin Buzzard (Jan 28 2019 at 16:56):

negreal is exactly what you've defined it to be.

#### Kevin Buzzard (Jan 28 2019 at 16:57):

It's not _equal_ to posreal.

#### Kevin Buzzard (Jan 28 2019 at 16:57):

It does biject with posreal, but then again the naturals biject with the integers.

#### Kevin Buzzard (Jan 28 2019 at 16:58):

As an exercise, you should import `data.equiv.basic`

and try and construct a term of type `equiv posreal negreal`

. There's your paint job.

#### Joseph Corneli (Jan 28 2019 at 16:58):

cool! Will look. :painting:

Last updated: May 12 2021 at 08:14 UTC