Commit 2022-11-23 19:36 f017f329

View on Github →

feat: port Logic.Equiv.Basic (#631) mathlib SHA: c3019c79074b0619edb4b27553a91b2e82242395 [I think this is right..?] WIP

depends on: #550

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Defs.lean

Created Mathlib/Init/Data/Sigma/Basic.lean

added theorem ex_of_psig

Created Mathlib/Logic/Equiv/Basic.lean

added theorem Equiv.Perm.eq_of_prodExtendRight_ne

added def Equiv.Perm.extendDomain

added theorem Equiv.Perm.extendDomain_apply_image

added theorem Equiv.Perm.extendDomain_apply_not_subtype

added theorem Equiv.Perm.extendDomain_apply_subtype

added theorem Equiv.Perm.extendDomain_refl

added theorem Equiv.Perm.extendDomain_symm

added theorem Equiv.Perm.extendDomain_trans

added theorem Equiv.Perm.fst_prodExtendRight

added def Equiv.Perm.prodExtendRight

added theorem Equiv.Perm.prodExtendRight_apply_eq

added theorem Equiv.Perm.prodExtendRight_apply_ne

added theorem Equiv.Perm.subtypeCongr.apply

added theorem Equiv.Perm.subtypeCongr.left_apply

added theorem Equiv.Perm.subtypeCongr.left_apply_subtype

added theorem Equiv.Perm.subtypeCongr.refl

added theorem Equiv.Perm.subtypeCongr.right_apply

added theorem Equiv.Perm.subtypeCongr.right_apply_subtype

added theorem Equiv.Perm.subtypeCongr.symm

added theorem Equiv.Perm.subtypeCongr.trans

added def Equiv.Perm.subtypeCongr

added def Equiv.Perm.sumCongr

added theorem Equiv.Perm.sumCongr_apply

added theorem Equiv.Perm.sumCongr_refl

added theorem Equiv.Perm.sumCongr_refl_swap

added theorem Equiv.Perm.sumCongr_swap_refl

added theorem Equiv.Perm.sumCongr_symm

added theorem Equiv.Perm.sumCongr_trans

added theorem Equiv.apply_swap_eq_self

added def Equiv.arrowProdEquivProdArrow

added def Equiv.boolArrowEquivProd

added def Equiv.boolEquivPUnitSumPUnit

added def Equiv.boolProdEquivSum

added theorem Equiv.coe_piCongr'

added theorem Equiv.coe_piCongr_symm

added theorem Equiv.coe_prodComm

added theorem Equiv.coe_prodUnique

added theorem Equiv.coe_subtypeEquivCodomain

added theorem Equiv.coe_subtypeEquivCodomain_symm

added theorem Equiv.coe_uniqueProd

added theorem Equiv.comp_swap_eq_update

added def Equiv.curry

added def Equiv.emptyProd

added def Equiv.emptySum

added theorem Equiv.emptySum_apply_inr

added def Equiv.funSplitAt

added def Equiv.intEquivNatSumNat

added theorem Equiv.isEmpty_congr

added def Equiv.listEquivOfEquiv

added def Equiv.natEquivNatSumPUnit

added def Equiv.natSumPUnitEquivNat

added theorem Equiv.ofBijective_apply_symm_apply

added theorem Equiv.ofBijective_symm_apply_apply

added def Equiv.ofFiberEquiv

added theorem Equiv.ofFiberEquiv_map

added def Equiv.optionEquivSumPUnit

added theorem Equiv.optionEquivSumPUnit_coe

added theorem Equiv.optionEquivSumPUnit_none

added theorem Equiv.optionEquivSumPUnit_some

added theorem Equiv.optionEquivSumPUnit_symm_inl

added theorem Equiv.optionEquivSumPUnit_symm_inr

added def Equiv.optionIsSomeEquiv

added def Equiv.pemptyProd

added def Equiv.piComm

added theorem Equiv.piComm_symm

added def Equiv.piCongr'

added theorem Equiv.piCongr'_apply

added theorem Equiv.piCongr'_symm_apply_symm_apply

added def Equiv.piCongr

added def Equiv.piCongrLeft'

added def Equiv.piCongrLeft

added def Equiv.piCongrRight

added theorem Equiv.piCongr_apply_apply

added theorem Equiv.piCongr_symm_apply

added def Equiv.piCurry

added def Equiv.piEquivPiSubtypeProd

added def Equiv.piEquivSubtypeSigma

added def Equiv.piOptionEquivProd

added def Equiv.piSplitAt

added def Equiv.pprodCongr

added def Equiv.pprodEquivProd

added def Equiv.pprodEquivProdPLift

added def Equiv.pprodProd

added def Equiv.prodAssoc

added def Equiv.prodComm

added theorem Equiv.prodComm_apply

added theorem Equiv.prodComm_symm

added def Equiv.prodCongr

added def Equiv.prodCongrLeft

added theorem Equiv.prodCongrLeft_apply

added theorem Equiv.prodCongrLeft_trans_prodComm

added def Equiv.prodCongrRight

added theorem Equiv.prodCongrRight_apply

added theorem Equiv.prodCongrRight_trans_prodComm

added theorem Equiv.prodCongr_refl_left

added theorem Equiv.prodCongr_refl_right

added theorem Equiv.prodCongr_symm

added def Equiv.prodEmpty

added def Equiv.prodPEmpty

added def Equiv.prodPProd

added def Equiv.prodPUnit

added def Equiv.prodShear

added def Equiv.prodSumDistrib

added theorem Equiv.prodSumDistrib_apply_left

added theorem Equiv.prodSumDistrib_apply_right

added theorem Equiv.prodSumDistrib_symm_apply_left

added theorem Equiv.prodSumDistrib_symm_apply_right

added def Equiv.prodUnique

added theorem Equiv.prodUnique_apply

added theorem Equiv.prodUnique_symm_apply

added def Equiv.psumCongr

added def Equiv.psumEquivSum

added def Equiv.psumSum

added def Equiv.punitProd

added theorem Equiv.semiconj_conj

added theorem Equiv.semiconj₂_conj

added def Equiv.setValue

added theorem Equiv.setValue_eq

added theorem Equiv.sigmaCongrRight_sigmaEquivProd

added theorem Equiv.sigmaEquivProd_sigmaCongrRight

added def Equiv.sigmaFiberEquiv

added def Equiv.sigmaNatSucc

added def Equiv.sigmaOptionEquivOfSome

added def Equiv.sigmaProdDistrib

added def Equiv.sigmaSubtypeEquivOfSubset

added def Equiv.sigmaSubtypeFiberEquiv

added def Equiv.sigmaSubtypeFiberEquivSubtype

added def Equiv.sigmaSumDistrib

added def Equiv.subtypeCongr

added def Equiv.subtypeEquiv

added def Equiv.subtypeEquivCodomain

added theorem Equiv.subtypeEquivCodomain_apply

added theorem Equiv.subtypeEquivCodomain_symm_apply

added theorem Equiv.subtypeEquivCodomain_symm_apply_eq

added theorem Equiv.subtypeEquivCodomain_symm_apply_ne

added def Equiv.subtypeEquivOfSubtype'

added def Equiv.subtypeEquivOfSubtype

added def Equiv.subtypeEquivProp

added def Equiv.subtypeEquivRight

added theorem Equiv.subtypeEquiv_apply

added theorem Equiv.subtypeEquiv_refl

added theorem Equiv.subtypeEquiv_symm

added theorem Equiv.subtypeEquiv_trans

added def Equiv.subtypePiEquivPi

added def Equiv.subtypePreimage

added theorem Equiv.subtypePreimage_symm_apply_coe_neg

added theorem Equiv.subtypePreimage_symm_apply_coe_pos

added def Equiv.subtypeProdEquivProd

added def Equiv.subtypeProdEquivSigmaSubtype

added def Equiv.subtypeQuotientEquivQuotientSubtype

added theorem Equiv.subtypeQuotientEquivQuotientSubtype_mk

added theorem Equiv.subtypeQuotientEquivQuotientSubtype_symm_mk

added def Equiv.subtypeSigmaEquiv

added def Equiv.subtypeSubtypeEquivSubtype

added def Equiv.subtypeSubtypeEquivSubtypeExists

added def Equiv.subtypeSubtypeEquivSubtypeInter

added def Equiv.subtypeUnivEquiv

added def Equiv.sumArrowEquivProdArrow

added theorem Equiv.sumArrowEquivProdArrow_apply_fst

added theorem Equiv.sumArrowEquivProdArrow_apply_snd

added theorem Equiv.sumArrowEquivProdArrow_symm_apply_inl

added theorem Equiv.sumArrowEquivProdArrow_symm_apply_inr

added def Equiv.sumAssoc

added theorem Equiv.sumAssoc_apply_inl_inl

added theorem Equiv.sumAssoc_apply_inl_inr

added theorem Equiv.sumAssoc_apply_inr

added theorem Equiv.sumAssoc_symm_apply_inl

added theorem Equiv.sumAssoc_symm_apply_inr_inl

added theorem Equiv.sumAssoc_symm_apply_inr_inr

added def Equiv.sumComm

added theorem Equiv.sumComm_symm

added def Equiv.sumCompl

added theorem Equiv.sumCompl_apply_inl

added theorem Equiv.sumCompl_apply_inr

added theorem Equiv.sumCompl_apply_symm_of_neg

added theorem Equiv.sumCompl_apply_symm_of_pos

added def Equiv.sumCongr

added theorem Equiv.sumCongr_refl

added theorem Equiv.sumCongr_symm

added theorem Equiv.sumCongr_trans

added def Equiv.sumEmpty

added theorem Equiv.sumEmpty_apply_inl

added def Equiv.sumEquivSigmaBool

added def Equiv.sumPSum

added def Equiv.sumProdDistrib

added theorem Equiv.sumProdDistrib_apply_left

added theorem Equiv.sumProdDistrib_apply_right

added theorem Equiv.sumProdDistrib_symm_apply_left

added theorem Equiv.sumProdDistrib_symm_apply_right

added def Equiv.swap

added def Equiv.swapCore

added theorem Equiv.swapCore_comm

added theorem Equiv.swapCore_self

added theorem Equiv.swapCore_swapCore

added theorem Equiv.swap_apply_def

added theorem Equiv.swap_apply_eq_iff

added theorem Equiv.swap_apply_left

added theorem Equiv.swap_apply_ne_self_iff

added theorem Equiv.swap_apply_of_ne_of_ne

added theorem Equiv.swap_apply_right

added theorem Equiv.swap_apply_self

added theorem Equiv.swap_comm

added theorem Equiv.swap_comp_apply

added theorem Equiv.swap_eq_refl_iff

added theorem Equiv.swap_eq_update

added theorem Equiv.swap_self

added theorem Equiv.swap_swap

added theorem Equiv.symm_swap

added theorem Equiv.symm_trans_swap_trans

added theorem Equiv.trans_swap_trans_symm

added def Equiv.uniqueCongr

added def Equiv.uniqueProd

added theorem Equiv.uniqueProd_apply

added theorem Equiv.uniqueProd_symm_apply

added theorem Function.Injective.map_swap

added theorem Function.Injective.swap_apply

added theorem Function.Injective.swap_comp

added theorem Function.Involutive.coe_toPerm

added def Function.Involutive.toPerm

added theorem Function.Involutive.toPerm_involutive

added theorem Function.Involutive.toPerm_symm

added theorem Function.piCongrLeft'_symm_update

added theorem Function.piCongrLeft'_update

added theorem Function.update_apply_equiv_apply

added theorem Function.update_comp_equiv

added theorem PLift.eq_up_iff_down_eq

added def equivOfSubsingletonOfSubsingleton

added def subsingletonProdSelfEquiv

added def uniqueUniqueEquiv

Modified Mathlib/Logic/Equiv/Defs.lean

added def Equiv.Simps.apply

added theorem Equiv.coe_fn_mk

added theorem Equiv.left_inv'

added theorem Equiv.right_inv'

Modified Mathlib/Order/Compare.lean

deleted theorem Ordering.Compares_eq

deleted theorem Ordering.Compares_gt

deleted theorem Ordering.Compares_lt

added theorem Ordering.compares_eq

added theorem Ordering.compares_gt

added theorem Ordering.compares_lt

Modified Mathlib/Order/Monotone.lean

modified theorem antitoneOn_toDual_comp_iff

modified theorem antitone_toDual_comp_iff

modified theorem monotoneOn_toDual_comp_iff

modified theorem monotone_toDual_comp_iff

modified theorem strictAntiOn_toDual_comp_iff

modified theorem strictAnti_toDual_comp_iff

modified theorem strictMonoOn_toDual_comp_iff

modified theorem strictMono_toDual_comp_iff

Modified Mathlib/Order/Synonym.lean