Theorems · Theorem
Function.rightInverse_surjInv
∀ {α : Sort u} {β : Sort v} {f : α → β} (hf : Function.Surjective f), Function.RightInverse (Function.surjInv hf) f- Defined in
- Mathlib.Logic.Function.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.surjInvstatement · cited by 63
- Function.surjInv_eqproof · cited by 18
Cited by12
Results whose statement or proof uses this declaration.
- Function.bijective_iff_has_inverseproof · cited by 50
- Function.injective_surjInvproof · cited by 14
- Function.Surjective.hasRightInverseproof · cited by 10
- Finite.injective_iff_surjectiveproof · cited by 9
- Function.Surjective.piMapproof · cited by 6
- Function.leftInverse_surjInvproof · cited by 2
- Topology.IsQuotientMap.lift_compproof · cited by 2
- Module.Basis.sumQuot_inrproof · cited by 2
- Setoid.quotientKerEquivOfSurjectiveproof · cited by 1
- Finsupp.mapDomain_surjectiveproof · cited by 1
- OreLocalization.cardinalMk_le_lift_cardinalMk_of_commuteproof · cited by 0
- AddOreLocalization.cardinalMk_le_lift_cardinalMk_of_addCommuteproof · cited by 0