Stream: new members

Topic: nat_ceil

Iocta (Jul 08 2020 at 23:42):

import data.real.basic

example : nat_ceil (1:real)  = (1:nat) :=
_


How to fill this?

Shing Tak Lam (Jul 09 2020 at 00:08):

Here's a solution, but I'm not sure if it's optimal

example : nat_ceil (1:real)  = (1:nat) :=
begin
rw show (1 : ℝ) = ↑(1 : ℕ), by norm_num,
rw nat_ceil_coe,
end


Bryan Gin-ge Chen (Jul 09 2020 at 00:13):

Here's another solution:

import data.real.basic

example : nat_ceil (1 : real) = (1 : nat) :=
begin
convert nat_ceil_coe 1,
rw [nat.cast_one],
end


Bryan Gin-ge Chen (Jul 09 2020 at 00:14):

Oh wait, this works:

example : nat_ceil (1 : real) = (1 : nat) :=
by rw [←nat.cast_one, nat_ceil_coe]


Johan Commelin (Jul 09 2020 at 04:07):

Can we write down a general statement for numerals? Doesn't seem to be trivial.

Kenny Lau (Jul 09 2020 at 04:17):

import data.real.basic

example : nat_ceil (1 : ℝ) = (1 : ℕ) :=
@nat.cast_one ℝ _ _ ▸ nat_ceil_coe 1

example : nat_ceil (1 : ℝ) = (1 : ℕ) :=
by exact_mod_cast @nat_ceil_coe ℝ _ _ 1


Kenny Lau (Jul 09 2020 at 04:18):

Johan Commelin said:

Can we write down a general statement for numerals? Doesn't seem to be trivial.

what do you mean?

Jason Orendorff (Jul 09 2020 at 12:00):

Johan Commelin said:

Can we write down a general statement for numerals? Doesn't seem to be trivial.

Isn't nat_ceil_coe that general statement? If you write nat_ceil_coe 5, the result is that nat_ceil (5 : ℝ) = 5.

Last updated: Dec 20 2023 at 11:08 UTC