Theorems · Theorem
Function.invFun_surjective
∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β},
Function.Injective f → Function.Surjective (Function.invFun f)- Defined in
- Mathlib.Logic.Function.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 15 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.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Function.invFunstatement · cited by 60
- Function.LeftInverse.surjectiveproof · cited by 22
- Function.leftInverse_invFunproof · cited by 13
Cited by9
Results whose statement or proof uses this declaration.
- exists_surjective_natproof · cited by 10
- Fintype.ofInjectiveproof · cited by 3
- not_injective_of_ordinalproof · cited by 2
- rank_fun_infiniteproof · cited by 2
- Cardinal.sum_lt_prodproof · cited by 1
- Finite.card_eq_zero_of_injectiveproof · cited by 1
- Function.exists_surjective_iffproof · cited by 0
- ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomialproof · cited by 0
- nonempty_embedding_to_cardinalproof · cited by 0