Commit 2022-11-13 23:57 719ea42c

View on Github →

chore: renaming and alignment for various definitions and lemmas (#572)

Estimated changes

Modified Mathlib/Data/FunLike/Equiv.lean

Modified Mathlib/Init/Function.lean

added theorem Function.HasLeftInverse.injective

added def Function.HasLeftInverse

added theorem Function.HasRightInverse.surjective

added def Function.HasRightInverse

deleted theorem Function.LeftInverse_of_surjective_of_RightInverse

deleted theorem Function.RightInverse_of_injective_of_LeftInverse

deleted theorem Function.has_LeftInverse.injective

deleted def Function.has_LeftInverse

deleted theorem Function.has_RightInverse.surjective

deleted def Function.has_RightInverse

added theorem Function.leftInverse_of_surjective_of_rightInverse

added theorem Function.rightInverse_of_injective_of_leftInverse

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.Bijective.existsUnique_iff

deleted theorem Function.Bijective.exists_unique_iff

added theorem Function.Injective.hasLeftInverse

deleted theorem Function.Injective.has_left_inverse

added theorem Function.LeftInverse.eq_rightInverse

deleted theorem Function.LeftInverse.eq_right_inverse

added theorem Function.LeftInverse.rightInverse_of_injective

added theorem Function.LeftInverse.rightInverse_of_surjective

deleted theorem Function.LeftInverse.right_inverse_of_injective

deleted theorem Function.LeftInverse.right_inverse_of_surjective

added theorem Function.RightInverse.leftInverse_of_injective

added theorem Function.RightInverse.leftInverse_of_surjective

deleted theorem Function.RightInverse.left_inverse_of_injective

deleted theorem Function.RightInverse.left_inverse_of_surjective

added theorem Function.Surjective.hasRightInverse

deleted theorem Function.Surjective.has_right_inverse

added theorem Function.bijective_iff_existsUnique

deleted theorem Function.bijective_iff_exists_unique

added theorem Function.injective_iff_hasLeftInverse

deleted theorem Function.injective_iff_has_left_inverse

added theorem Function.injective_of_isPartialInv

added theorem Function.injective_of_isPartialInv_right

deleted theorem Function.injective_of_partial_inv

deleted theorem Function.injective_of_partial_inv_right

added theorem Function.injective_surjInv

deleted theorem Function.injective_surj_inv

added theorem Function.invFun_comp

added theorem Function.invFun_eq

added theorem Function.invFun_eq_of_injective_of_rightInverse

added theorem Function.invFun_neg

added theorem Function.invFun_surjective

deleted theorem Function.inv_fun_comp

deleted theorem Function.inv_fun_eq

deleted theorem Function.inv_fun_eq_of_injective_of_right_inverse

deleted theorem Function.inv_fun_neg

deleted theorem Function.inv_fun_surjective

added theorem Function.isPartialInv_left

deleted theorem Function.is_partial_inv_left

added theorem Function.leftInverse_iff_comp

added theorem Function.leftInverse_invFun

added theorem Function.leftInverse_surjInv

deleted theorem Function.left_inverse_iff_comp

deleted theorem Function.left_inverse_inv_fun

deleted theorem Function.left_inverse_surj_inv

added theorem Function.partialInv_left

added theorem Function.partialInv_of_injective

deleted theorem Function.partial_inv_left

deleted theorem Function.partial_inv_of_injective

added theorem Function.rightInverse_iff_comp

added theorem Function.rightInverse_invFun

added theorem Function.rightInverse_surjInv

deleted theorem Function.right_inverse_iff_comp

deleted theorem Function.right_inverse_inv_fun

deleted theorem Function.right_inverse_surj_inv

added theorem Function.surjInv_eq

deleted theorem Function.surj_inv_eq

added theorem Function.surjective_iff_hasRightInverse

deleted theorem Function.surjective_iff_has_right_inverse

Modified Mathlib/Logic/Function/Conjugate.lean

added theorem Function.Semiconj₂.isAssociative_left

added theorem Function.Semiconj₂.isAssociative_right

added theorem Function.Semiconj₂.isIdempotent_left

added theorem Function.Semiconj₂.isIdempotent_right

deleted theorem Function.Semiconj₂.is_associative_left

deleted theorem Function.Semiconj₂.is_associative_right

deleted theorem Function.Semiconj₂.is_idempotent_left

deleted theorem Function.Semiconj₂.is_idempotent_right