Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-08 14:49 8ef8f819

View on Github →

feat(data/equiv): port data/equiv.lean from Lean2

Estimated changes

Created data/equiv.lean

added theorem equiv.apply_eq_iff_eq

added theorem equiv.apply_eq_iff_eq_inverse_apply

added def equiv.arrow_arrow_equiv_prod_arrow

added def equiv.arrow_congr

added def equiv.arrow_prod_equiv_prod_arrow

added def equiv.arrow_unit_equiv_unit

added def equiv.bool_equiv_unit_sum_unit

added def equiv.bool_prod_equiv_sum

added theorem equiv.comp_apply

added def equiv.decidable_eq_of_equiv

added def equiv.empty_arrow_equiv_unit

added theorem equiv.eq_iff_eq_of_injective

added theorem equiv.eq_of_to_fun_eq

added def equiv.false_arrow_equiv_unit

added def equiv.false_equiv_empty

added def equiv.fn

added def equiv.id

added theorem equiv.id_apply

added def equiv.inhabited_of_equiv

added def equiv.inv

added theorem equiv.inverse_apply_apply

added def equiv.nat_equiv_nat_sum_unit

added def equiv.nat_sum_bool_equiv_nat

added def equiv.nat_sum_unit_equiv_nat

added def equiv.perm

added def equiv.prod_assoc

added def equiv.prod_comm

added def equiv.prod_congr

added def equiv.prod_empty_left

added def equiv.prod_empty_right

added def equiv.prod_sum_distrib

added def equiv.prod_unit_left

added def equiv.prod_unit_right

added def equiv.subtype_equiv_of_subtype

added def equiv.sum_arrow_equiv_prod_arrow

added def equiv.sum_assoc

added def equiv.sum_comm

added def equiv.sum_congr

added def equiv.sum_empty_left

added def equiv.sum_empty_right

added def equiv.sum_prod_distrib

added def equiv.swap

added theorem equiv.swap_apply_def

added theorem equiv.swap_apply_left

added theorem equiv.swap_apply_of_ne_of_ne

added theorem equiv.swap_apply_right

added theorem equiv.swap_comm

added theorem equiv.swap_comp_apply

added def equiv.swap_core

added theorem equiv.swap_core_comm

added theorem equiv.swap_core_self

added theorem equiv.swap_core_swap_core

added theorem equiv.swap_self

added theorem equiv.swap_swap

added def equiv.unit_arrow_equiv

added structure equiv

added theorem function.left_inverse.f_g_eq_id

added theorem function.right_inverse.g_f_eq_id

added def subtype.map

added theorem subtype.map_comp

added theorem subtype.map_id