Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-08 06:22 8bdb1474

View on Github →

feat(topology/local_homeomorph): local homeomorphisms (#1398)

feat(topology/local_homeomorph): local homeomorphisms
local_homeomorph: reviewer comments

Estimated changes

Created src/topology/local_homeomorph.lean

added theorem homeomorph.refl_to_local_homeomorph

added theorem homeomorph.symm_to_local_homeomorph

added def homeomorph.to_local_homeomorph

added theorem homeomorph.to_local_homeomorph_inv_fun

added theorem homeomorph.to_local_homeomorph_source

added theorem homeomorph.to_local_homeomorph_target

added theorem homeomorph.to_local_homeomorph_to_fun

added theorem homeomorph.trans_to_local_homeomorph

added theorem local_homeomorph.apply_eq_of_eq_on_source

added theorem local_homeomorph.continuous_on_iff_continuous_on_comp_left

added theorem local_homeomorph.continuous_on_iff_continuous_on_comp_right

added theorem local_homeomorph.eq_of_eq_on_source_univ

added theorem local_homeomorph.eq_of_local_equiv_eq

added def local_homeomorph.eq_on_source

added theorem local_homeomorph.eq_on_source_iff

added theorem local_homeomorph.eq_on_source_refl

added theorem local_homeomorph.eq_on_source_restr

added theorem local_homeomorph.eq_on_source_symm

added theorem local_homeomorph.eq_on_source_trans

added theorem local_homeomorph.image_trans_source

added theorem local_homeomorph.inv_apply_eq_of_eq_on_source

added theorem local_homeomorph.inv_image_trans_target

added def local_homeomorph.of_set

added theorem local_homeomorph.of_set_inv_fun

added theorem local_homeomorph.of_set_source

added theorem local_homeomorph.of_set_symm

added theorem local_homeomorph.of_set_target

added theorem local_homeomorph.of_set_to_fun

added theorem local_homeomorph.of_set_to_local_equiv

added theorem local_homeomorph.of_set_trans'

added theorem local_homeomorph.of_set_trans

added theorem local_homeomorph.preimage_interior

added def local_homeomorph.prod

added theorem local_homeomorph.prod_inv_fun

added theorem local_homeomorph.prod_source

added theorem local_homeomorph.prod_target

added theorem local_homeomorph.prod_to_fun

added theorem local_homeomorph.prod_to_local_equiv

added theorem local_homeomorph.refl_inv_fun

added theorem local_homeomorph.refl_local_equiv

added theorem local_homeomorph.refl_source

added theorem local_homeomorph.refl_symm

added theorem local_homeomorph.refl_target

added theorem local_homeomorph.refl_to_fun

added theorem local_homeomorph.refl_trans

added theorem local_homeomorph.restr_eq_of_source_subset

added theorem local_homeomorph.restr_inv_fun

added theorem local_homeomorph.restr_open_source

added theorem local_homeomorph.restr_open_to_local_equiv

added theorem local_homeomorph.restr_source'

added theorem local_homeomorph.restr_source

added theorem local_homeomorph.restr_source_inter

added theorem local_homeomorph.restr_target

added theorem local_homeomorph.restr_to_fun

added theorem local_homeomorph.restr_to_local_equiv'

added theorem local_homeomorph.restr_to_local_equiv

added theorem local_homeomorph.restr_trans

added theorem local_homeomorph.restr_univ

added theorem local_homeomorph.source_eq_of_eq_on_source

added theorem local_homeomorph.symm_inv_fun

added theorem local_homeomorph.symm_source

added theorem local_homeomorph.symm_symm

added theorem local_homeomorph.symm_target

added theorem local_homeomorph.symm_to_fun

added theorem local_homeomorph.symm_to_local_equiv

added theorem local_homeomorph.target_eq_of_eq_on_source

added theorem local_homeomorph.trans_assoc

added theorem local_homeomorph.trans_inv_fun

added theorem local_homeomorph.trans_of_set'

added theorem local_homeomorph.trans_of_set

added theorem local_homeomorph.trans_refl

added theorem local_homeomorph.trans_self_symm

added theorem local_homeomorph.trans_source''

added theorem local_homeomorph.trans_source'

added theorem local_homeomorph.trans_source

added theorem local_homeomorph.trans_symm_eq_symm_trans_symm

added theorem local_homeomorph.trans_symm_self

added theorem local_homeomorph.trans_target''

added theorem local_homeomorph.trans_target'

added theorem local_homeomorph.trans_target

added theorem local_homeomorph.trans_to_fun

added theorem local_homeomorph.trans_to_local_equiv

added structure local_homeomorph