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