topology eq of homeomorph

Stream: Is there code for X?

[Adam Topaz]

Do we have something like the following "evil" lemma?

import topology.homeomorph

variables {α : Type*} (t1 t2 : topological_space α)

lemma topological_space.eq_of_homeo_id (f : @homeomorph α α t1 t2)
  (is_id : ∀ a : α, f a = a) : t1 = t2 := sorry

[Johan Commelin]

I wouldn't be surprised if it's not there.

[Adam Topaz]

Meh, I can probably just get by with docs#homeomorph.inducing in my case.