Show that the inverse function is continuous

Stream: new members

[Daniele Bolla]

Hello there, i am pretty new to lean and Mathlib and would need some help.
I am trying to prove that the inverse function 1/x is continuous on the positive reals, but i am stuck.

in particular i wan to use ContinuousOn.inv₀ but not sure how.
I was thinking to use refine, but getting some errors.
Here the code: https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQP0CmIIScwAdgG4BiAruQJIDOAwhOTBbRLUwPLkAChCYAlAknRwAXHDYcuPfuTgAKAGb04ADxlxAuIRwAvAD4dgbwIAnQEo1AZQIwAdAwjA4ABlvSjcLAE8cODgoAnUKAgByOXZOcm5eAScKSkAAgiA.

DONE.
I've actually do it like this:

import Mathlib

lemma invFunIsContinuousOnPosReal : ContinuousOn (fun x : ℝ => x⁻¹) (Set.Ioi 0) := by
  apply ContinuousOn.inv₀
  · exact continuous_id.continuousOn
  · intro x hx
    exact ne_of_gt hx

[Notification Bot]

Daniele Bolla has marked this topic as resolved.