from rationals to reals

Stream: Is there code for X?

[Jeremy Avigad]

Suppose f and g are continuous functions from reals to reals and they are equal on the rationals. How do I show they are equal on the reals?

[Johan Commelin]

docs#dense_range.equalizer

[Johan Commelin]

Maybe together with rat.dense_embedding_coe_real.dense

[Matt Diamond]

there's also docs#rat.dense_range_cast