missing homeomorphism ‌‌/ DilationEquiv API

Stream: Is there code for X?

[Jireh Loreaux]

It seems to me we are missing some API related to homeomorphisms. In particular, I couldn't find things like these:

import Mathlib.Analysis.NormedSpace.IsROrC

def DilationEquiv.toHomeomorph {X Y : Type*} [PseudoEMetricSpace X] [PseudoEMetricSpace Y]
    (e : X ≃ᵈ Y) : X ≃ₜ Y where
  continuous_toFun := Dilation.toContinuous e
  continuous_invFun := Dilation.toContinuous e.symm
  __ := e.toEquiv

@[simp]
lemma DilationEquiv.coe_toHomeomorph {X Y : Type*} [PseudoEMetricSpace X] [PseudoEMetricSpace Y]
    {e : X ≃ᵈ Y} : ⇑e.toHomeomorph = e :=
  rfl

@[simp]
lemma DilationEquiv.toHomeomorph_symm {X Y : Type*} [PseudoEMetricSpace X]
    [PseudoEMetricSpace Y] {e : X ≃ᵈ Y} : e.toHomeomorph.symm = e.symm.toHomeomorph :=
  rfl

open NNReal

@[simps]
def NormedSpace.dilationEquiv (𝕜 : Type*) {E : Type*} [IsROrC 𝕜] [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] (y : E) {r : ℝ} (hr : 0 < r) :
    E ≃ᵈ E where
  toFun w := (‖r‖ : 𝕜) • w + y
  invFun w := (‖r‖⁻¹ : 𝕜) • (w - y)
  left_inv w := by simp [smul_smul, inv_mul_cancel (show ((|r| : ℝ) : 𝕜) ≠ 0 by simpa using hr.ne')]
  right_inv w := by simp [smul_smul, mul_inv_cancel (show ((|r| : ℝ) : 𝕜) ≠ 0 by simpa using hr.ne')]
  edist_eq' := by
    lift r to ℝ≥0 using hr.le
    simp only [ne_eq, Real.norm_eq_abs, edist_add_right]
    refine ⟨r, by exact_mod_cast hr.ne', fun w₁ w₁ ↦ ?_⟩
    simp only [NNReal.abs_eq, edist_eq_coe_nnnorm_sub, ← smul_sub, sub_sub_sub_cancel_right,
      nnnorm_smul, ENNReal.coe_mul]
    norm_cast
    ext
    simp

def Homeomorph.subtype {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {p : X → Prop}
    {q : Y → Prop} (e : X ≃ₜ Y) (he : ∀ x, p x ↔ q (e x)) :
    {x // p x} ≃ₜ {y // q y} where
  toFun := Subtype.map e (he · |>.mp)
  invFun := Subtype.map e.symm fun y hy ↦ he _ |>.mpr ((e.apply_symm_apply y).symm ▸ hy)
  left_inv x := by ext; simp
  right_inv y := by ext; simp
  continuous_toFun := by simp only; exact e.continuous.subtype_map _
  continuous_invFun := by simp only; exact e.symm.continuous.subtype_map _

def Homeomorph.sets {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X}
    {t : Set Y} (e : X ≃ₜ Y) (he : s = e ⁻¹' t) :
    s ≃ₜ t :=
  Homeomorph.subtype e <| Set.ext_iff.mp he

[Eric Wieser]

Does linking to continuous affine equivs make sense here?

[Jireh Loreaux]

Do we have those?

[Yury G. Kudryashov]

As for NormedSpace.dilationEquiv, I think that translation and multiplication should be separate defs. Also, one of them is an IsometryEquiv. I don't know if we have IsometryEquiv.toDilationEquiv.

[Eric Wieser]

Huh, we only have docs#ContinuousAffineMap and docs#AffineEquiv