Zulip Chat Archive

Stream: new members

Topic: nat_ceil


view this post on Zulip Iocta (Jul 08 2020 at 23:42):

import data.real.basic

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

How to fill this?

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

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

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

view this post on Zulip Johan Commelin (Jul 09 2020 at 04:07):

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

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

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

view this post on Zulip 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: May 10 2021 at 00:31 UTC