Theorems · Theorem
Function.invFun_eq
∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β} {b : β}, (∃ a, f a = b) → f (Function.invFun f b) = b- Defined in
- Mathlib.Logic.Function.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 13 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.
- Classical.arbitraryproof · cited by 161
- Function.invFunstatement · cited by 60
Cited by10
Results whose statement or proof uses this declaration.
- Function.leftInverse_invFunproof · cited by 13
- Function.apply_invFun_applyproof · cited by 5
- lift_trdeg_le_of_surjectiveproof · cited by 3
- Function.rightInverse_invFunproof · cited by 3
- Metric.totallyBounded_of_finite_discretizationproof · cited by 2
- AkraBazziRecurrence.sumCoeffsExp_p_eq_oneproof · cited by 2
- Function.Embedding.schroeder_bernstein_of_relproof · cited by 2
- Function.invFun_eq_of_injective_of_rightInverseproof · cited by 0
- Function.Embedding.invFun_restrictproof · cited by 0
- Function.Injective.invFun_restrictproof · cited by 0