Functions with various real domains

Stream: new members

[Notification Bot]

Callum Cassidy-Nolan has marked this topic as unresolved.

[Callum Cassidy-Nolan]

If I had a function defined on R \to \R then how could I state that that function is increasing only for 3 < x ? I'm using strict_mono for increasing function.

[Jireh Loreaux]

I think strict_mono is quantified over the whole type. So, you could roll your own strictly increasing statement for 3 < x, or you could use a subtype (the former will be preferable).

[Callum Cassidy-Nolan]

What about if I simply wanted a function who's domain was all reals except zero? Is there a way to encode this in the functions type itself?

[Jireh Loreaux]

Subtypes: { x : real // x ≠ 0}. The downside is that you don't get all the theorems about real numbers because this subtype isn't the real numbers. Often it's better to just give your function a "garbage value" where you don't have a definition. Then the function is still total, and it's still defined on the real numbers. Then, in your theorems about that function, you just add the hypothesis x≠0.

[Kevin Buzzard]

A great example is the inverse function on the reals sending x to x⁻¹. In lean we have 0⁻¹ = 0 rather than defining inverse only on nonzero elements. It turns out to be much less painful this way.

[Yaël Dillies]

Callum Cassidy-Nolan said:

If I had a function defined on R → \R then how could I state that that function is increasing only for 3 < x ? I'm using strict_mono for increasing function.

docs#strict_mono_on

[Jireh Loreaux]

Oh, I forgot about that. Nice.