Zulip Chat Archive

Stream: new members

Topic: Show that the inverse function is continuous


Daniele Bolla (Apr 03 2025 at 12:40):

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 (Apr 03 2025 at 12:50):

Daniele Bolla has marked this topic as resolved.


Last updated: May 02 2025 at 03:31 UTC