Positive real numbers

Stream: new members

[Martin Dvořák]

What is the best way to define a function f : ℝ → ℝ but with positive real numbers only as both its domain and its codomain? I want f : ℝ^+ → ℝ^+ or something like that. At some point, I will want to claim that f is injective.

[Yaël Dillies]

Either define stuff as junk value and use docs#set.inj_on, or use docs#nnreal, or write the API for preal :wink:

[Violeta Hernández]

Unless it's completely nonsensical, you might want to consider defining f such that f 0 = 0 and f (-x) = - f x

[Violeta Hernández]

It's a simple way to guarantee injectivity while not having to deal with subtypes

[Violeta Hernández]

But it might not be suited to your problem

[Martin Dvořák]

What is the best way of formalizing it if I want to argue about a function f : ℝ^+ → ℝ^+ being injective, but I need to perform some of the intermediate calculations in real numbers?

[Eric Wieser]

Can you give a mwe?

[Damiano Testa]

Without knowing what exactly the shape of f is, it is difficult to know what might work.

For instance, if you replace your f by log ∘ f ∘ exp, then you have a function from ℝ → ℝ which is injective (or monotone) iff your original f is. Would this be useful?

[Martin Dvořák]

Eric Wieser said:

Can you give a mwe?

I'll think about it.