Zulip Chat Archive

Stream: new members

Topic: homeomorph.trans

Nicolò Cavalleri (Aug 30 2020 at 15:40):

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 (Aug 30 2020 at 15:52):

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 (Aug 30 2020 at 15:55):

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

Nicolò Cavalleri (Aug 30 2020 at 16:03):

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

Last updated: Dec 20 2023 at 11:08 UTC