Theorems · Theorem
Function.Bijective.surjective
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Bijective f → Function.Surjective f- Defined in
- Mathlib.Logic.Function.Basic
- Cited by
- 114 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 6 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
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
Cited by115
Results whose statement or proof uses this declaration.
- Equiv.ofBijectiveproof · cited by 70
- Matrix.det_mulproof · cited by 51
- Function.Bijective.of_comp_iffproof · cited by 22
- MulOpposite.op_surjectiveproof · cited by 21
- Function.bijective_iff_existsUniqueproof · cited by 15
- AddOpposite.op_surjectiveproof · cited by 12
- MulOpposite.unop_surjectiveproof · cited by 11
- Function.Bijective.existsUnique_iffproof · cited by 8
- AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrankproof · cited by 6
- MulAction.isPreprimitive_congrproof · cited by 6
- AddOpposite.unop_surjectiveproof · cited by 6
- MulAction.surjectiveproof · cited by 5