Zulip Chat Archive

Stream: new members

Topic: Inequalities and coercions


view this post on Zulip Donald Sebastian Leung (Feb 29 2020 at 03:59):

In the standard library, there is a lemma int.coe_nat_le_coe_nat_of_le which states that one can coerce both sides of an inequality involving natural numbers to get an inequality involving integers. Is there a similar lemma which performs lifting from the natural numbers to the reals?

view this post on Zulip Kevin Buzzard (Feb 29 2020 at 08:09):

There is probably one which works for maps from the naturals to arbitrary totally ordered semirings or something, and you might be able to find it with library_search if you just copy the statement of the lemma above and replace the ints with reals. The reason ints are treated differently is some consequences of a design decision, something about the canonical map from the naturals to the integers being a constructor.

view this post on Zulip Kevin Buzzard (Feb 29 2020 at 08:11):

I should also say that the whole point of tactics like norm_cast is to enable the user to not have to ask questions like this. Your question reminds me of the old days

view this post on Zulip Kevin Buzzard (Feb 29 2020 at 08:12):

The lemma name might have the word cast in rather thancoe , I never worked out the difference

view this post on Zulip Donald Sebastian Leung (Feb 29 2020 at 08:56):

Kevin Buzzard said:

I should also say that the whole point of tactics like norm_cast is to enable the user to not have to ask questions like this. Your question reminds me of the old days

Thanks, using norm_cast made my life much easier :stuck_out_tongue:


Last updated: May 16 2021 at 21:11 UTC