Commit 2022-11-02 22:22 ecd46453

View on Github →

feat: port Logic.Function.Basic (#511)

Estimated changes

Modified Mathlib/Init/Function.lean

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Logic/Function/Basic.lean

added theorem Bool.involutive_not

added theorem Function.Bijective.comp_left

added theorem Function.Bijective.comp_right

deleted theorem Function.Bijective.exists_unique

added theorem Function.Bijective.exists_unique_iff

modified theorem Function.Bijective.of_comp_iff'

modified theorem Function.Bijective.of_comp_iff

added theorem Function.Injective.comp_left

deleted def Function.Injective.decidable_eq

modified theorem Function.Injective.eq_iff'

modified theorem Function.Injective.eq_iff

deleted theorem Function.Injective.has_LeftInverse

added theorem Function.Injective.has_left_inverse

modified theorem Function.Injective.ne

modified theorem Function.Injective.ne_iff'

modified theorem Function.Injective.ne_iff

modified theorem Function.Injective.of_comp

modified theorem Function.Injective.of_comp_iff'

modified theorem Function.Injective.of_comp_iff

added theorem Function.Injective.surjective_comp_right'

added theorem Function.Injective.surjective_comp_right

modified theorem Function.Injective2.eq_iff

added theorem Function.Injective2.left'

added theorem Function.Injective2.right'

modified def Function.Injective2

modified theorem Function.Involutive.comp_self

modified def Function.Involutive

added def Function.IsPartialInv

deleted theorem Function.LeftInverse.RightInverse

added theorem Function.LeftInverse.cast_eq

modified theorem Function.LeftInverse.comp

deleted theorem Function.LeftInverse.eq_RightInverse

added theorem Function.LeftInverse.eq_rec_eq

added theorem Function.LeftInverse.eq_rec_on_eq

added theorem Function.LeftInverse.eq_right_inverse

added theorem Function.LeftInverse.rightInverse

added theorem Function.LeftInverse.right_inverse_of_injective

added theorem Function.LeftInverse.right_inverse_of_surjective

modified theorem Function.LeftInverse.surjective

deleted theorem Function.LeftInverse_iff_comp

deleted theorem Function.LeftInverse_inv_fun

deleted theorem Function.LeftInverse_surj_inv

deleted theorem Function.RightInverse.LeftInverse

modified theorem Function.RightInverse.comp

modified theorem Function.RightInverse.injective

added theorem Function.RightInverse.leftInverse

added theorem Function.RightInverse.left_inverse_of_injective

added theorem Function.RightInverse.left_inverse_of_surjective

deleted theorem Function.RightInverse_iff_comp

deleted theorem Function.RightInverse_inv_fun

deleted theorem Function.RightInverse_surj_inv

added theorem Function.Surjective.comp_left

deleted theorem Function.Surjective.exists

deleted theorem Function.Surjective.exists₂

deleted theorem Function.Surjective.exists₃

deleted theorem Function.Surjective.forall

deleted theorem Function.Surjective.forall₂

deleted theorem Function.Surjective.forall₃

deleted theorem Function.Surjective.has_RightInverse

added theorem Function.Surjective.has_right_inverse

added theorem Function.Surjective.injective_comp_right

modified theorem Function.Surjective.of_comp

modified theorem Function.Surjective.of_comp_iff'

modified theorem Function.Surjective.of_comp_iff

added theorem Function.apply_extend

modified theorem Function.apply_update

added theorem Function.apply_update₂

modified theorem Function.bijective_iff_exists_unique

modified theorem Function.bijective_iff_has_inverse

modified theorem Function.cantor_injective

modified theorem Function.cantor_surjective

modified theorem Function.comp_const

modified theorem Function.comp_update

modified theorem Function.const_comp

modified theorem Function.const_def

added theorem Function.const_inj

added theorem Function.const_injective

modified theorem Function.curry_apply

modified theorem Function.eq_update_iff

added theorem Function.eval_apply

added theorem Function.exists_update_iff

added def Function.extend

modified theorem Function.extend_apply

modified theorem Function.extend_comp

modified theorem Function.extend_def

added theorem Function.extend_injective

modified theorem Function.funext_iff

modified theorem Function.id_def

deleted theorem Function.injective_iff_has_LeftInverse

added theorem Function.injective_iff_has_left_inverse

modified theorem Function.injective_of_partial_inv

modified theorem Function.injective_of_partial_inv_right

modified theorem Function.injective_of_subsingleton

modified theorem Function.injective_surj_inv

modified theorem Function.inv_fun_comp

modified theorem Function.inv_fun_eq

deleted theorem Function.inv_fun_eq_of_injective_of_RightInverse

added theorem Function.inv_fun_eq_of_injective_of_right_inverse

modified theorem Function.inv_fun_neg

deleted theorem Function.inv_fun_on_eq'

deleted theorem Function.inv_fun_on_eq

deleted theorem Function.inv_fun_on_mem

deleted theorem Function.inv_fun_on_neg

deleted theorem Function.inv_fun_on_pos

modified theorem Function.inv_fun_surjective

modified theorem Function.involutive_iff_iter_2_eq_id

deleted def Function.is_partial_inv

modified theorem Function.is_partial_inv_left

added theorem Function.left_inverse_iff_comp

added theorem Function.left_inverse_inv_fun

added theorem Function.left_inverse_surj_inv

added theorem Function.ne_iff

added theorem Function.not_surjective_Type

modified theorem Function.partial_inv_left

modified theorem Function.partial_inv_of_injective

added theorem Function.right_inverse_iff_comp

added theorem Function.right_inverse_inv_fun

added theorem Function.right_inverse_surj_inv

modified theorem Function.sometimes_spec

modified theorem Function.surj_inv_eq

added theorem Function.surjective_eval

deleted theorem Function.surjective_iff_has_RightInverse

added theorem Function.surjective_iff_has_right_inverse

added theorem Function.surjective_of_right_cancellable_Prop

modified theorem Function.surjective_to_subsingleton

modified theorem Function.uncurry_apply_pair

modified theorem Function.uncurry_bicompl

modified theorem Function.uncurry_bicompr

modified theorem Function.uncurry_def

modified def Function.update

modified theorem Function.update_apply

modified theorem Function.update_comm

modified theorem Function.update_comp_eq_of_forall_ne'

modified theorem Function.update_comp_eq_of_forall_ne

modified theorem Function.update_comp_eq_of_injective'

modified theorem Function.update_comp_eq_of_injective

modified theorem Function.update_eq_iff

modified theorem Function.update_eq_self

modified theorem Function.update_idem

modified theorem Function.update_injective

modified theorem Function.update_noteq

modified theorem Function.update_same

added theorem InvImage.equivalence

added theorem IsSymmOp.flip_eq

added def Set.SeparatesPoints

added def Set.piecewise

added theorem cast_bijective

added theorem cast_inj

added theorem eq_mp_bijective

added theorem eq_mpr_bijective

added theorem eq_rec_inj

added theorem eq_rec_on_bijective

deleted def set.piecewise

deleted def set.separates_points