Theorems · Theorem
Function.leftInverse_invFun
∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β},
Function.Injective f → Function.LeftInverse (Function.invFun f) f- Defined in
- Mathlib.Logic.Function.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Nonempty
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.invFunstatement and proof · cited by 60
- Function.invFun_eqproof · cited by 10
Cited by14
Results whose statement or proof uses this declaration.
- Equiv.ofInjectiveproof · cited by 64
- Function.invFun_surjectiveproof · cited by 8
- LinearMap.exists_leftInverse_of_injectiveproof · cited by 6
- AddMonoidAlgebra.coeff_supDegree_add_supDegreeproof · cited by 5
- Function.Injective.hasLeftInverseproof · cited by 4
- AddMonoidAlgebra.leadingCoeff_singleproof · cited by 2
- Function.invFun_compproof · cited by 2
- small_of_injective_of_existsproof · cited by 2
- Function.Embedding.schroeder_bernstein_of_relproof · cited by 2
- AddMonoidAlgebra.supDegree_mem_supportproof · cited by 1
- groupHomology.H1CoresCoinf_exactproof · cited by 0
- Set.preimage_invFun_of_memproof · cited by 0