Theorems · Theorem
Function.bijective_iff_existsUnique
∀ {α : Sort u_1} {β : Sort u_2} (f : α → β), Function.Bijective f ↔ ∀ (b : β), ∃! a, f a = b- Defined in
- Mathlib.Logic.Function.Basic
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.Bijectivestatement and proof · cited by 863
- ExistsUniquestatement and proof · cited by 268
- Function.Bijective.injectiveproof · cited by 115
- Function.Bijective.surjectiveproof · cited by 114
- ExistsUnique.uniqueproof · cited by 42
- ExistsUnique.existsproof · cited by 26
Cited by15
Results whose statement or proof uses this declaration.
- Function.Bijective.existsUniqueproof · cited by 7
- Subgroup.isComplement_iff_existsUniqueproof · cited by 4
- AddSubgroup.isComplement_iff_existsUniqueproof · cited by 3
- CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafConditionproof · cited by 3
- Subgroup.isComplement_subgroup_left_iff_bijectiveproof · cited by 2
- Subgroup.isComplement_subgroup_right_iff_bijectiveproof · cited by 2
- CategoryTheory.Presieve.isSheafFor_of_preservesProductproof · cited by 2
- AddSubgroup.isComplement_addSubgroup_left_iff_bijectiveproof · cited by 2
- AddSubgroup.isComplement_addSubgroup_right_iff_bijectiveproof · cited by 2
- CategoryTheory.regularTopology.EqualizerCondition.mkproof · cited by 2
- CategoryTheory.isCodetector_iff_reflectsIsomorphisms_yoneda_objproof · cited by 0