Commit 2022-10-24 23:24 d411237a

View on Github →

chore: capitalise Injective (#501) We had previously been changing mathport output to write Function.injective rather than Function.Injective. At https://github.com/leanprover-community/mathlib4/pull/498#discussion_r1003840030 @digama0 pointed out that mathport is capitalising correctly here. This PR re-capitalises Injective, Surjective, Bijective, and Involutive, all in the Function namespace.

Estimated changes

modified theorem div_left_injective
modified theorem div_right_injective
modified theorem inv_injective
modified theorem inv_involutive
modified theorem inv_surjective
modified theorem mul_left_surjective
modified theorem mul_right_surjective
modified theorem CommGroup.toGroup_injective
modified theorem mul_left_injective
modified theorem mul_right_injective
modified theorem List.append_left_injective
modified theorem List.append_right_injective
modified theorem List.cons_injective
modified theorem List.length_injective
modified theorem List.length_injective_iff
modified theorem List.mem_map_of_injective
modified theorem Option.map_injective
modified theorem Option.some_injective
modified theorem Prod.fst_injective
modified theorem Prod.fst_surjective
modified theorem Prod.snd_injective
modified theorem Prod.snd_surjective
modified theorem Prod.swap_bijective
modified theorem Prod.swap_injective
modified theorem Prod.swap_surjective
modified theorem sigma_mk_injective
modified theorem Subtype.coe_injective
modified theorem Subtype.restrict_injective
modified theorem Subtype.val_injective
deleted theorem Function.bijective.comp
deleted def Function.bijective
modified theorem Function.bijective_id
deleted theorem Function.injective.comp
deleted def Function.injective
modified theorem Function.injective_id
deleted theorem Function.surjective.comp
deleted def Function.surjective
modified theorem Function.surjective_id
modified theorem PLift.down_injective
modified theorem ULift.down_injective
added theorem Function.Injective.ne
modified theorem Function.cantor_surjective
modified theorem Function.extend_apply
modified theorem Function.extend_comp
deleted theorem Function.injective.dite
deleted theorem Function.injective.eq_iff
deleted theorem Function.injective.ne
deleted theorem Function.injective.ne_iff
deleted def Function.injective2
modified theorem Function.injective_surj_inv
modified theorem Function.inv_fun_comp
modified theorem Function.inv_fun_surjective
deleted def Function.involutive
modified theorem Function.partial_inv_left
modified theorem Function.surj_inv_eq
modified theorem Function.update_injective
modified def LinearOrder.lift
modified def PartialOrder.lift
modified theorem Preorder.to_le_injective