real affine maps

Stream: Is there code for X?

[Rémi Bottinelli]

Hey! I've got two reals a ≤ b and need to show that the affine map f sending 0 to a and 1 to b satisfies:

• monotone_on f (Icc 0 1)
• surj_on f (Icc 0 1) (Icc a b)
• mapsto f (Icc 0 1) (Icc a b)

Is it already done somewhere?

[Eric Wieser]

Are you looking for docs#affine_map.line_map?