monotone inverse le

Stream: new members

[Iocta]

Is there something like (h : monotone g) (h' : g(x) <= y) : x <= (inverse g) y?

[Iocta]

And maybe the antitone version too?

[Ruben Van de Velde]

Try writing a #mwe first

[Aaron Liu]

docs#GaloisConnection seems similar

[Kevin Buzzard]

Yeah but it's impossible to say anything coherent because we don't know the types of anything or any of the assumptions until we have a #mwe

[Iocta]

import Mathlib


example (g : ℝ → ℝ) (h : Monotone g) (x y : ℝ) : g x ≤ y ↔ x ≤ g⁻¹ y := sorry

example (g : ℝ → ℝ) (h : Antitone g) (x y : ℝ) : g x ≤ y ↔ x ≥ g⁻¹ y := sorry

[Eric Wieser]

g⁻¹ is the function fun x => (g x)⁻¹; is that what you intended?

[Iocta]

No

[Iocta]

I mean the function inverse

[Aaron Liu]

What if the inverse doesn't exist?

[Iocta]

Well it needs to exist

[Aaron Liu]

Sometimes it doesn't exist. How do you prevent someone from applying this theorem to a function that doesn't have an inverse?

[Eric Wieser]

What's the inverse of g = (fun x => 3)?

[Iocta]

I imagine there's an "inverse function" concept somewhere in mathlib, and it has the necessary hypotheses?

[Iocta]

Or not?

[Matt Diamond]

docs#Function.invFun

[Matt Diamond]

it only requires that the domain is nonempty, so you should be fine with ℝ → ℝ

[Matt Diamond]

is g Surjective?

[Iocta]

Let's say yes for now

[Matt Diamond]

if it is, there's also docs#Function.surjInv

[Iocta]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Filter/Pointwise.html#Filter.inv_le_inv_iff seems closeish to the statement I wanted

[Aaron Liu]

Those f and g in docs#Filter.inv_le_inv_iff are pointwise inverse on the filters, so not what you want.

[Matt Diamond]

@Iocta if you had an OrderIso you could just use docs#OrderIso.le_symm_apply

[Yaël Dillies]

If you don't have an OrderIso, then the concept of "inverse" is very nicely captured by docs#GaloisConnection