Skip to content

Linear interpolation on proper closed real intervals#1972

Draft
malarbol wants to merge 3 commits into
UniMath:masterfrom
malarbol:linear-interpolation-proper-closed-interval
Draft

Linear interpolation on proper closed real intervals#1972
malarbol wants to merge 3 commits into
UniMath:masterfrom
malarbol:linear-interpolation-proper-closed-interval

Conversation

@malarbol

@malarbol malarbol commented Jun 4, 2026

Copy link
Copy Markdown
Collaborator

This PR introduces the concept of linear interpolation w.r.t. to a proper closed interval of real numbers [a, b], as the map

  t ↦ (b - a) * t + a

and its inverse

  x ↦ (x - a)/(b - a)

This is essentially a refactoring of the content of uniform-homeomorphism-unit-interval-proper-closed-interval-real-numbers (credits to @lowasser) to give a proper name to the uniform homeomorphism considered there.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant