Wrenna Robson

I will note that we only have one instance of floor_semiring currently, which feels... off.

Oh yes, sorry. I wasn't counting the two in the floor.lean file itself because I'd already fixed them! `nnrat` is derivable like `nnreal` from the nonneg instance so I'll just...

If you think that's best. On Wed, 12 Oct 2022, 07:04 Yaël Dillies, ***@***.***> wrote: > ***@***.**** commented on this pull request. > ------------------------------ > > In counterexamples/map_floor.lean > >...

Can you think of a better name for `floor_of_not_nonneg`?

Added some more generalisations. I feel like `ceil_add_nat` should be able to be proved without the linearity, but I cannot see how.

Sorry, I've not had the time to work on this as much. Mistake I think. On Wed, 19 Oct 2022, 16:44 Yaël Dillies, ***@***.***> wrote: > ***@***.**** commented on this...

Shall I abandon this?

I don't see any reason to keep this open now.

I will freely admit I don't entirely understand the bornology stuff or why it's necessary. Bearing that in mind: This is good I think, but ultimately I do not think...

I'd be happy if you renamed `discrete` to `const`. It's also probably true that there is more to be said about discreteness - for instance, a metric can be discrete...