Commit 2022-12-14 13:31 18fa17a0

View on Github →

feat port: Data.PEquiv (#1008) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/PEquiv.lean

added def Equiv.toPEquiv

added theorem Equiv.toPEquiv_apply

added theorem Equiv.toPEquiv_refl

added theorem Equiv.toPEquiv_symm

added theorem Equiv.toPEquiv_trans

added theorem PEquiv.bot_apply

added theorem PEquiv.bot_trans

added theorem PEquiv.coe_mk_apply

added theorem PEquiv.eq_some_iff

added theorem PEquiv.ext

added theorem PEquiv.ext_iff

added theorem PEquiv.injective_of_forall_is_some

added theorem PEquiv.injective_of_forall_ne_isSome

added theorem PEquiv.is_some_symm_get

added theorem PEquiv.le_def

added theorem PEquiv.mem_iff_mem

added theorem PEquiv.mem_ofSet_iff

added theorem PEquiv.mem_ofSet_self_iff

added theorem PEquiv.mem_single

added theorem PEquiv.mem_single_iff

added theorem PEquiv.mem_trans

added def PEquiv.ofSet

added theorem PEquiv.ofSet_eq_refl

added theorem PEquiv.ofSet_eq_some_iff

added theorem PEquiv.ofSet_eq_some_self_iff

added theorem PEquiv.ofSet_symm

added theorem PEquiv.ofSet_univ

added theorem PEquiv.refl_apply

added theorem PEquiv.refl_trans

added theorem PEquiv.self_trans_symm

added def PEquiv.single

added theorem PEquiv.single_apply

added theorem PEquiv.single_apply_of_ne

added theorem PEquiv.single_subsingleton_eq_refl

added theorem PEquiv.single_trans_of_eq_none

added theorem PEquiv.single_trans_of_mem

added theorem PEquiv.single_trans_single

added theorem PEquiv.single_trans_single_of_ne

added theorem PEquiv.symm_bot

added theorem PEquiv.symm_injective

added theorem PEquiv.symm_refl

added theorem PEquiv.symm_single

added theorem PEquiv.symm_symm

added theorem PEquiv.symm_trans_rev

added theorem PEquiv.symm_trans_self

added theorem PEquiv.trans_assoc

added theorem PEquiv.trans_bot

added theorem PEquiv.trans_eq_none

added theorem PEquiv.trans_eq_some

added theorem PEquiv.trans_refl

added theorem PEquiv.trans_single_of_eq_none

added theorem PEquiv.trans_single_of_mem

added theorem PEquiv.trans_symm_eq_iff_forall_is_some

added structure PEquiv