Commit 2021-07-09 12:32 2ea02e95

View on Github →

feat(Logic/Function) port everything up to partial_inv_left (#24)

Estimated changes

Modified Mathlib/Logic/Basic.lean

added def decidable_of_iff

added theorem iff_of_eq

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.bijective.exists_unique

added theorem Function.bijective.of_comp_iff'

added theorem Function.bijective.of_comp_iff

added theorem Function.bijective_iff_exists_unique

added theorem Function.cantor_injective

added theorem Function.cantor_surjective

added theorem Function.comp_apply

added theorem Function.comp_const

added theorem Function.const_apply

added theorem Function.const_comp

added theorem Function.const_def

added def Function.eval

added theorem Function.eval_apply

added theorem Function.funext_iff

added theorem Function.hfunext

added theorem Function.id_def

added def Function.injective.decidable_eq

added theorem Function.injective.dite

added theorem Function.injective.eq_iff'

added theorem Function.injective.eq_iff

added theorem Function.injective.ne

added theorem Function.injective.ne_iff'

added theorem Function.injective.ne_iff

added theorem Function.injective.of_comp

added theorem Function.injective.of_comp_iff'

added theorem Function.injective.of_comp_iff

added theorem Function.injective_of_partial_inv

added theorem Function.injective_of_partial_inv_right

added theorem Function.injective_of_subsingleton

added def Function.is_partial_inv

added theorem Function.is_partial_inv_left

added theorem Function.left_inverse.comp_eq_id

added theorem Function.left_inverse.eq_right_inverse

added theorem Function.left_inverse.right_inverse

added theorem Function.left_inverse.surjective

added theorem Function.left_inverse_iff_comp

added theorem Function.partial_inv_left

added theorem Function.partial_inv_of_injective

added theorem Function.right_inverse.comp_eq_id

added theorem Function.right_inverse.injective

added theorem Function.right_inverse.left_inverse

added theorem Function.right_inverse_iff_comp

added theorem Function.surjective.exists

added theorem Function.surjective.exists₂

added theorem Function.surjective.exists₃

added theorem Function.surjective.forall

added theorem Function.surjective.forall₂

added theorem Function.surjective.forall₃

added theorem Function.surjective.of_comp

added theorem Function.surjective.of_comp_iff'

added theorem Function.surjective.of_comp_iff