Lipschitz_Equivalent_Metric_Spaces_are_Homeomorphic_v2
Provedhomeomorphic-metric-spaceslipschitz-equivalenceproofwiki
If two metric spaces are Lipschitz equivalent (bijection with bi-Lipschitz bounds), then they are homeomorphic.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Lipschitz_Equivalent_Metric_Spaces_are_Homeomorphic_v2 {α : Type _} {β : Type _} [MetricSpace α] [MetricSpace β] (f : α → β) (g : β → α) (h : ∃ K > 0, ∀ x y : α, dist (f x) (f y) ≤ K * dist x y) (h2 : ∃ K > 0, ∀ x y : β, dist (g x) (g y) ≤ K * dist x y) (hfg : ∀ x, g (f x) = x) (hgf : ∀ y, f (g y) = y) : Continuous f ∧ Continuous g := by sorrySource