# Zulip Chat Archive

## Stream: new members

### Topic: Coercions

#### Frédéric Le Roux (Jan 03 2020 at 18:56):

I have two questions about coercions :

1) Is there a direct way to go from `0:nat < 2:nat`

to `0:real < 2:real`

?

2) I have a type X, E is of type `set X`

, and `x : \N \to E`

, is there a way to see x as a sequence in X rather than in E? `\u x`

does not seem to work.

The context is that I have a defintion of limit in X and I would like to apply it to sequences in E. Of course I can declare `x: \N \to X`

and add the property that every value of x is in E, but I guess coercions are designed to do the job.

#### Patrick Massot (Jan 03 2020 at 19:01):

Your first question is a bit vague, but maybe it is answered by the following snippet:

import data.real.basic example (h : 0 < 2) : (0 : ℝ) < 2 := begin -- exact h won't work exact_mod_cast h, end

#### Patrick Massot (Jan 03 2020 at 19:02):

I guess this example was oversimplified but, just in case, the "right" way of proving `(0 : ℝ) < 2`

is to use the `norm_num`

tactic.

#### Kevin Buzzard (Jan 03 2020 at 19:21):

As for the second question, you might well find that `x 3`

is a pair, consisting of (1) a term of type `X`

and (2) a proof that this term is in `E`

. So perhaps `(x 3).1`

will be the element of `X`

that you're looking for.

#### Kevin Buzzard (Jan 03 2020 at 19:34):

To make matters even more confusing (at least for a beginner), if `E : set X`

then `E`

is a term, not a type, and so `e : E`

doesn't really make sense (and neither does `\N \to E`

). However it's OK, because there is something called a subtype of X, and what happens is that when Lean sees you want to think about `E`

as a type it coerces it magically to be the subtype. This is the difference between `{x : \N | x > 6}`

and `{x : \N // x > 6}`

(the first is the subset, the second is the subtype). The coercion is indicated by the little up-arrow `\u`

.

Last updated: May 12 2021 at 23:13 UTC