Homeomorphisms between [0,1] and [a,b]?

Stream: Is there code for X?

[Scott Morrison]

Do we have the homeomorphisms between different (non-trivial) closed intervals in real?

[Scott Morrison]

(and by "the" I mean I specifically want the affine homeomorphisms, but I want them bundled as a ≃ₜ)

[Scott Morrison]

Failing that, just the fact that a * x + b is a homeomorphism of real to itself when a is nonzero.

[Anatole Dedecker]

I can't find it, but composing docs#homeomorph.mul_left' and and docs#homeomorph.add_right should do it