homeomorph.trans

Stream: new members

[Nicolò Cavalleri]

I am not sure if these kind of lemmas are missing from mathlib or it is me who is not still able to find things, or if I am stating things the wrong way.

example {α : Type*} {β : Type*} [topological_space α] [topological_space β] (e : α ≃ₜ β) :
  e.trans e.symm = homeomorph.refl α := by library_search!

(I'd guess this should contain trans_symm in the name if it existed?)

[Alex J. Best]

I can't see it in mathlib, you should copy the names of the versions in data/equiv/basic.lean  I guess where there is

@[simp] theorem refl_trans (e : α ≃ β) : (equiv.refl α).trans e = e := by { cases e, refl }

@[simp] theorem symm_trans (e : α ≃ β) : e.symm.trans e = equiv.refl β := ext (by simp)

@[simp] theorem trans_symm (e : α ≃ β) : e.trans e.symm = equiv.refl α := ext (by simp)

and more.

[Nicolò Cavalleri]

Ok thanks! Weird cause symm_trans is there for local homeomorphs in a more complicated version.

[Nicolò Cavalleri]

I am also surprised to see there is no extensionality rule for homeomorph