Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-28 08:37 cbf4740a

View on Github →

refactor(data/equiv/local_equiv): use dot notation for eq_on_source (#2830) Also reuse more lemmas from data/set/function.

Estimated changes

Modified src/data/equiv/local_equiv.lean

deleted theorem local_equiv.apply_eq_of_eq_on_source

added theorem local_equiv.eq_on_source.eq_on

added theorem local_equiv.eq_on_source.restr

added theorem local_equiv.eq_on_source.source_eq

added theorem local_equiv.eq_on_source.source_inter_preimage_eq

added theorem local_equiv.eq_on_source.symm'

added theorem local_equiv.eq_on_source.symm_eq_on

added theorem local_equiv.eq_on_source.target_eq

added theorem local_equiv.eq_on_source.trans'

deleted theorem local_equiv.eq_on_source_preimage

deleted theorem local_equiv.eq_on_source_restr

deleted theorem local_equiv.eq_on_source_symm

deleted theorem local_equiv.eq_on_source_trans

deleted theorem local_equiv.inv_apply_eq_of_eq_on_source

deleted theorem local_equiv.source_eq_of_eq_on_source

added theorem local_equiv.symm_maps_to

deleted theorem local_equiv.target_eq_of_eq_on_source

Modified src/data/set/function.lean

deleted theorem set.eq_on_of_left_inv_of_right_inv

added theorem set.eq_on_of_left_inv_on_of_right_inv_on

Modified src/geometry/manifold/manifold.lean

Modified src/topology/local_homeomorph.lean

deleted theorem local_homeomorph.apply_eq_of_eq_on_source

added theorem local_homeomorph.eq_on_source.eq_on

added theorem local_homeomorph.eq_on_source.restr

added theorem local_homeomorph.eq_on_source.source_eq

added theorem local_homeomorph.eq_on_source.symm'

added theorem local_homeomorph.eq_on_source.symm_eq_on_target

added theorem local_homeomorph.eq_on_source.target_eq

added theorem local_homeomorph.eq_on_source.trans'

deleted theorem local_homeomorph.eq_on_source_restr

deleted theorem local_homeomorph.eq_on_source_symm

deleted theorem local_homeomorph.eq_on_source_trans

deleted theorem local_homeomorph.inv_apply_eq_of_eq_on_source

deleted theorem local_homeomorph.source_eq_of_eq_on_source

deleted theorem local_homeomorph.target_eq_of_eq_on_source

Modified src/topology/topological_fiber_bundle.lean