Theorem LipschitzWith.inv

Modification history

2024-06-19 13:47

Mathlib/Analysis/Normed/Group/Basic.lean

feat: `f⁻¹` is continuous iff `f` is (#13951) …

Deleted LipschitzWith.inv View on Github →

2023-03-09 06:58

Mathlib/Analysis/Normed/Group/Basic.lean

feat: port Analysis.Normed.Group.Basic (#2736)

Added LipschitzWith.inv View on Github →