## Stream: new members

### Topic: How do I "cast" inequalities?

#### YH (Dec 13 2019 at 18:58):

If I have (1 ≤ n) as ℕ how do I get (1:ℝ)≤ ↑n? Library search didn't help.

#### Johan Commelin (Dec 13 2019 at 18:58):

norm_cast is supposed to help in such situations

#### Kevin Buzzard (Dec 13 2019 at 18:59):

import data.real.basic

example (n : ℕ) (h : 1 ≤ n) : (1 : ℝ) ≤ n :=
begin
exact_mod_cast h
end


#### Kevin Buzzard (Dec 13 2019 at 19:00):

Someone asked me this at Xena yesterday and I revised all the various flavours of norm_cast ;-)

Last updated: May 14 2021 at 22:15 UTC