Stream: Is there code for X?

Topic: homeo of induced by equiv

Adam Topaz (Dec 15 2020 at 21:14):

I'm working with the following minimal example:

import topology.constructions
import topology.homeomorph

namespace scratch

variables {α β : Type*} [topological_space β] (f : α  β)
instance : topological_space α := topological_space.induced f $by apply_instance example : α ≃ₜ β := sorry end scratch I have two questions here: 1. There is a maximum class-instance resolution depth error in the example. It seems lean is having trouble finding the topological space instances which I find strange. Why? 2. Does mathlib have the definition needed to fill in the sorry? Sebastien Gouezel (Dec 15 2020 at 21:20): The instance is a bad instance: it means that, whenever Lean is looking for a topological space structure on some type α, it will explore all types β and all equivs between the two types. There is no way to determine which one it should use. Adam Topaz (Dec 15 2020 at 21:20): Oh yes of course. Adam Topaz (Dec 15 2020 at 21:21): I should add fto a synonym for \a, for example. Sebastien Gouezel (Dec 15 2020 at 21:21): Yes, using a type synonym with the information on f would be enough to make things reasonable. Adam Topaz (Dec 15 2020 at 21:27): Okay, so here's an updated code: import topology.constructions import topology.homeomorph namespace scratch variables {α β : Type*} [topological_space β] (f : α β) include f def γ := α instance : topological_space (γ f) := topological_space.induced f$ by apply_instance
example : (γ f) ≃ₜ β := sorry

end scratch

Does mathlib have a quick way to fill in the sorry?

Yury G. Kudryashov (Dec 18 2020 at 23:25):

variables [topological_space β] (f : α  β)

def induced_space (f : α  β) := α

instance : topological_space (induced_space f) := topological_space.induced f \$ by apply_instance

example : (induced_space f) ≃ₜ β :=
{ to_equiv := f,
continuous_to_fun := continuous_induced_dom,
continuous_inv_fun := continuous_induced_rng (by simp [continuous_id]) }

Last updated: May 19 2021 at 00:40 UTC