Homeomorphism between empty sets (in different types)

Stream: Is there code for X?

[Michael Rothgang]

Given the empty set in two different types, does mathlib have the homeomorphism (or even the unique) function between these? MWE

import Mathlib
lemma emptyhom {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y}  (hs : s = ∅) (ht : t = ∅) : Homeomorph s t := sorry

Mathematically, this is obvious (there's a unique function between the empty sets; it's vacuously continuous at each point). I have a proof, but I'm sure this can be golfed much more - and have the itch this should exist somewhere. Loogle and moogle were not helpful, though.

[Michael Rothgang]

Current solution: improvements welcome!

lemma emptyhom {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y}
    (hs : s = ∅) (ht : t = ∅) : Homeomorph s t :=
  {
    toFun := fun ⟨x, hx⟩ ↦ ((Set.mem_empty_iff_false x).mp (hs ▸ hx)).elim
    invFun := fun ⟨x, hx⟩ ↦ ((Set.mem_empty_iff_false x).mp (ht ▸ hx)).elim
    left_inv := by intro; aesop
    right_inv := by intro; aesop
  }

[Ruben Van de Velde]

For what it's worth, mathlib doesn't usually have arguments that just state that a free variable is equal to something, like your hs and ht, as it tends to be easier to just substitute them

[Ruben Van de Velde]

And I'm guessing you should use def rather than lemma here

[Michael Rothgang]

Thanks: updated code

[Alex J. Best]

I guess I would expect this to be stated similarly to docs#Equiv.equivOfIsEmpty (which answers your question about the unique function also)

[Alex J. Best]

ie

import Mathlib
lemma emptyhom {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [IsEmpty X] [IsEmpty Y]: Homeomorph X Y :=
{ Equiv.equivOfIsEmpty X Y  with }

[Patrick Massot]

Ruben Van de Velde said:

For what it's worth, mathlib doesn't usually have arguments that just state that a free variable is equal to something, like your hs and ht, as it tends to be easier to just substitute them

It is true in general but it is worth saying this isn't always a good idea. It leads to a proliferation of ugly and slow calls to convert.

[Scott Morrison]

Michael Rothgang said:

Current solution: improvements welcome!

lemma emptyhom {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y}
    (hs : s = ∅) (ht : t = ∅) : Homeomorph s t :=
  {
    toFun := fun ⟨x, hx⟩ ↦ ((Set.mem_empty_iff_false x).mp (hs ▸ hx)).elim
    invFun := fun ⟨x, hx⟩ ↦ ((Set.mem_empty_iff_false x).mp (ht ▸ hx)).elim
    left_inv := by intro; aesop
    right_inv := by intro; aesop
  }

Someone really should put := by aesop as a default argument here!

[Michael Rothgang]

Thanks for all the feedback! I have PRed this lemmas a part of #8160.