Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-05 00:46 62928251

View on Github →

feat(data/equiv/local_equiv): define local equivalences (#1359)

feat(data/equiv/local_equiv): define local equivalences
add doc
add extensionality attribute
sanity_check

Estimated changes

Created src/data/equiv/local_equiv.lean

added theorem equiv.refl_to_local_equiv

added theorem equiv.symm_to_local_equiv

added def equiv.to_local_equiv

added theorem equiv.to_local_equiv_inv_fun

added theorem equiv.to_local_equiv_source

added theorem equiv.to_local_equiv_target

added theorem equiv.to_local_equiv_to_fun

added theorem equiv.trans_to_local_equiv

added theorem local_equiv.apply_eq_of_eq_on_source

added theorem local_equiv.bij_on_source

added theorem local_equiv.eq_of_eq_on_source_univ

added def local_equiv.eq_on_source

added theorem local_equiv.eq_on_source_preimage

added theorem local_equiv.eq_on_source_refl

added theorem local_equiv.eq_on_source_restr

added theorem local_equiv.eq_on_source_symm

added theorem local_equiv.eq_on_source_trans

added theorem local_equiv.image_eq_target_inter_inv_preimage

added theorem local_equiv.image_source_eq_target

added theorem local_equiv.image_trans_source

added theorem local_equiv.inv_apply_eq_of_eq_on_source

added theorem local_equiv.inv_image_eq_source_inter_preimage

added theorem local_equiv.inv_image_target_eq_source

added theorem local_equiv.inv_image_trans_target

added def local_equiv.of_set

added theorem local_equiv.of_set_inv_fun

added theorem local_equiv.of_set_source

added theorem local_equiv.of_set_symm

added theorem local_equiv.of_set_target

added theorem local_equiv.of_set_to_fun

added def local_equiv.prod

added theorem local_equiv.prod_inv_fun

added theorem local_equiv.prod_source

added theorem local_equiv.prod_target

added theorem local_equiv.prod_to_fun

added theorem local_equiv.refl_inv_fun

added theorem local_equiv.refl_restr_source

added theorem local_equiv.refl_restr_target

added theorem local_equiv.refl_source

added theorem local_equiv.refl_symm

added theorem local_equiv.refl_target

added theorem local_equiv.refl_to_fun

added theorem local_equiv.refl_trans

added theorem local_equiv.restr_eq_of_source_subset

added theorem local_equiv.restr_inv_fun

added theorem local_equiv.restr_source

added theorem local_equiv.restr_target

added theorem local_equiv.restr_to_fun

added theorem local_equiv.restr_trans

added theorem local_equiv.restr_univ

added theorem local_equiv.source_eq_of_eq_on_source

added theorem local_equiv.source_inter_preimage_inv_preimage

added theorem local_equiv.source_subset_preimage_target

added theorem local_equiv.symm_inv_fun

added theorem local_equiv.symm_source

added theorem local_equiv.symm_symm

added theorem local_equiv.symm_target

added theorem local_equiv.symm_to_fun

added theorem local_equiv.target_eq_of_eq_on_source

added theorem local_equiv.target_inter_inv_preimage_preimage

added theorem local_equiv.target_subset_preimage_source

added theorem local_equiv.trans_apply

added theorem local_equiv.trans_assoc

added theorem local_equiv.trans_inv_apply

added theorem local_equiv.trans_inv_fun

added theorem local_equiv.trans_refl

added theorem local_equiv.trans_refl_restr'

added theorem local_equiv.trans_refl_restr

added theorem local_equiv.trans_self_symm

added theorem local_equiv.trans_source''

added theorem local_equiv.trans_source'

added theorem local_equiv.trans_source

added theorem local_equiv.trans_symm_eq_symm_trans_symm

added theorem local_equiv.trans_symm_self

added theorem local_equiv.trans_target''

added theorem local_equiv.trans_target'

added theorem local_equiv.trans_target

added theorem local_equiv.trans_to_fun

added structure local_equiv