Inverse On vs inverse - for a property on a set

Stream: new members

[Michael Novak]

Given s : Set a and a function f : a → b, if I know that f.invFunOn s has some property on the set f '' s (for example ContinuousOn) can I infer that f.invFun also has that property on f '' s? And if so, how can we show it?

[Michael Novak]

For example is it possible to prove the following:

example (f : ℝ → ℝ) (s : Set ℝ) (h : ContinuousOn (f.invFunOn s) (f  '' s)) : ContinuousOn f.invFun (f  ' ' s) := sorry

[Vlad Tsyrklevich]

Your types are wrong, s has type Set a in Function.invFunOn and I don't think your h hypothesis says what you intend it to. and this does actually match what ContinuousOn expects, my mistake.

[Michael Novak]

You are right, thank you very much and sorry for the mistake. Does the question makes sense now after the edit?

[Vlad Tsyrklevich]

I don't think \^-1 is doing what you think it does here

example (f : ℝ → ℝ) (s : Set ℝ) (h : ContinuousOn (f.invFunOn s) s) : ContinuousOn f⁻¹ s := by
  have (a : s) : f⁻¹ a = 1 / (f a) := by
    simp

[Michael Novak]

Oh, I thought that f⁻¹ is notation for f.invFun, my bad. I edited the question once again.

[Vlad Tsyrklevich]

I don't think this is true (and I think the original statement for ContinuousOn on s not f '' s was correct.) f may map s and t into f '' s, but the mapping may only be continuous on s not t. The inverse is constructed by choice and so it may map backwards into t.

[Michael Novak]

What I actually want to show in the real proof I'm working on is to infer Set.BijOn (Function.invFun ψ) (ψ '' I) I from Set.BijOn (Function.invFunOn ψ I) (ψ '' I) I. Is that possible?

[Vlad Tsyrklevich]

If psi were injective, yes. But otherwise, psi inverse may map out of I.

[Michael Novak]

o.k., I understand. Thank you very much!