Commit 2024-06-19 13:47 63b99cae

View on Github →

feat: f⁻¹ is continuous iff f is (#13951) ... and similar results for lipschitzness. From LeanCamCombi

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Basic.lean

deleted theorem LipschitzWith.inv

added theorem antilipschitzWith_inv_iff

added theorem lipschitzOnWith_inv_iff

added theorem lipschitzWith_inv_iff

added theorem locallyLipschitz_inv_iff

Modified Mathlib/Topology/Algebra/Group/Basic.lean

added theorem continuousAt_inv_iff

added theorem continuousOn_inv_iff

added theorem continuous_inv_iff