Zulip Chat Archive

Stream: new members

Topic: How do I "cast" inequalities?


view this post on Zulip YH (Dec 13 2019 at 18:58):

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

view this post on Zulip Johan Commelin (Dec 13 2019 at 18:58):

norm_cast is supposed to help in such situations

view this post on Zulip 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

view this post on Zulip 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