Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-24 16:46 88f8de36

View on Github →

feat(topology/local_homeomorph): define helper definition (#14360)

Define homeomorph.trans_local_homeomorph and local_homeomorph.trans_homeomorph. They are equal to local_homeomorph.trans, but with better definitional behavior for source and target.
Define similar operations for local_equiv.
Use this to improve the definitional behavior of topological_fiber_bundle.trivialization.trans_fiber_homeomorph
Also use @[simps] to generate a couple of extra simp-lemmas.

Estimated changes

Modified src/logic/equiv/local_equiv.lean

modified def equiv.to_local_equiv

deleted theorem equiv.to_local_equiv_coe

deleted theorem equiv.to_local_equiv_source

deleted theorem equiv.to_local_equiv_symm_coe

deleted theorem equiv.to_local_equiv_target

added def equiv.trans_local_equiv

added theorem equiv.trans_local_equiv_eq_trans

modified def local_equiv.copy

modified def local_equiv.disjoint_union

modified def local_equiv.is_image.restr

deleted theorem local_equiv.pi_coe

deleted theorem local_equiv.pi_symm

modified def local_equiv.piecewise

added def local_equiv.trans_equiv

added theorem local_equiv.trans_equiv_eq_trans

Modified src/topology/fiber_bundle.lean

Modified src/topology/homeomorph.lean

added theorem homeomorph.coe_symm_to_equiv

Modified src/topology/local_homeomorph.lean

modified def homeomorph.to_local_homeomorph

deleted theorem homeomorph.to_local_homeomorph_coe_symm

added def homeomorph.trans_local_homeomorph

added theorem homeomorph.trans_local_homeomorph_eq_trans

added theorem local_homeomorph.to_local_equiv_injective

added theorem local_homeomorph.trans_equiv_eq_trans

added def local_homeomorph.trans_homeomorph