floats vs. reals

Stream: maths

[Dean Young]

Are floats in bijection with reals or are they actual floats taking up only so much memory? is π a float?

[Johan Commelin]

There is no bijection. float is not a ring.

[Eric Wieser]

Nor is there an injection; inf is not a real

[Kyle Miller]

I mean, you can take the 64-bit representation and inject it into Nat (edit: since float is not a ring, may as well ask if there's some injection since there's no structure to preserve)

[Kyle Miller]

@Kind Bubble This is a pretty open-ended question. Maybe you should read about floating-point numbers to learn about their basic properties? Lean implements the standard IEEE 754 floating point numbers as far as I know, which pretty much every programming language uses.

[Kevin Buzzard]

There are finitely many floats and uncountably many reals