Commit 2022-02-21 17:40 a7b020c7

View on Github →

chore: use the same names as in mathport (#200) Ideally this would cause mathport to align these definitions, and then we can translate the notation.

Estimated changes

Modified Mathlib/Data/Equiv/Basic.lean

modified def Equiv.symm

Modified Mathlib/Data/Equiv/Functor.lean

Modified Mathlib/Data/Prod.lean

added theorem Prod.swap_LeftInverse

added theorem Prod.swap_RightInverse

deleted theorem Prod.swap_left_inverse

deleted theorem Prod.swap_right_inverse

Modified Mathlib/Init/Function.lean

added theorem Function.LeftInverse.injective

added def Function.LeftInverse

added theorem Function.LeftInverse_of_surjective_of_RightInverse

added theorem Function.RightInverse.surjective

added def Function.RightInverse

added theorem Function.RightInverse_of_injective_of_LeftInverse

added theorem Function.has_LeftInverse.injective

added def Function.has_LeftInverse

added theorem Function.has_RightInverse.surjective

added def Function.has_RightInverse

deleted theorem Function.has_left_inverse.injective

deleted def Function.has_left_inverse

deleted theorem Function.has_right_inverse.surjective

deleted def Function.has_right_inverse

deleted theorem Function.left_inverse.injective

deleted def Function.left_inverse

deleted theorem Function.left_inverse_of_surjective_of_right_inverse

deleted theorem Function.right_inverse.surjective

deleted def Function.right_inverse

deleted theorem Function.right_inverse_of_injective_of_left_inverse

Modified Mathlib/Init/Logic.lean

added def RightInverse

deleted def right_inverse

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.LeftInverse.RightInverse

added theorem Function.LeftInverse.comp

added theorem Function.LeftInverse.comp_eq_id

added theorem Function.LeftInverse.eq_RightInverse

added theorem Function.LeftInverse.surjective

added theorem Function.LeftInverse_iff_comp

added theorem Function.LeftInverse_inv_fun

added theorem Function.LeftInverse_surj_inv

added theorem Function.RightInverse.LeftInverse

added theorem Function.RightInverse.comp

added theorem Function.RightInverse.comp_eq_id

added theorem Function.RightInverse.injective

added theorem Function.RightInverse_iff_comp

added theorem Function.RightInverse_inv_fun

added theorem Function.RightInverse_surj_inv

modified theorem Function.bijective_iff_has_inverse

added theorem Function.injective.has_LeftInverse

deleted theorem Function.injective.has_left_inverse

added theorem Function.injective_iff_has_LeftInverse

deleted theorem Function.injective_iff_has_left_inverse

modified theorem Function.inv_fun_comp

added theorem Function.inv_fun_eq_of_injective_of_RightInverse

deleted theorem Function.inv_fun_eq_of_injective_of_right_inverse

deleted theorem Function.left_inverse.comp

deleted theorem Function.left_inverse.comp_eq_id

deleted theorem Function.left_inverse.eq_right_inverse

deleted theorem Function.left_inverse.right_inverse

deleted theorem Function.left_inverse.surjective

deleted theorem Function.left_inverse_iff_comp

deleted theorem Function.left_inverse_inv_fun

deleted theorem Function.left_inverse_surj_inv

deleted theorem Function.right_inverse.comp

deleted theorem Function.right_inverse.comp_eq_id

deleted theorem Function.right_inverse.injective

deleted theorem Function.right_inverse.left_inverse

deleted theorem Function.right_inverse_iff_comp

deleted theorem Function.right_inverse_inv_fun

deleted theorem Function.right_inverse_surj_inv

added theorem Function.surjective.has_RightInverse

deleted theorem Function.surjective.has_right_inverse

added theorem Function.surjective_iff_has_RightInverse

deleted theorem Function.surjective_iff_has_right_inverse