Theorems · Definition
Equiv.funUnique
(α : Sort u) → (β : Sort u_1) → [Unique α] → (α → β) ≃ β
If α has a unique term, then the type of function α → β is equivalent to β.
- Defined in
- Mathlib.Logic.Equiv.Defs
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses Quot.sound
- Assumes
- Unique
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.
- Equivstatement · cited by 8,337
- Uniquestatement and proof · cited by 400
- Equiv.piUniqueproof · cited by 4
Cited by40
Results whose statement or proof uses this declaration.
- groupCohomology.cochainsIso₁proof · cited by 35
- groupHomology.chainsIso₁proof · cited by 33
- groupHomology.comp_d₂₁_eqproof · cited by 10
- groupCohomology.comp_d₁₂_eqproof · cited by 10
- Equiv.funUnique_applystatement and proof · cited by 7
- Equiv.subtypeEquivCodomainproof · cited by 7
- groupHomology.comp_d₁₀_eqproof · cited by 6
- OrderIso.funUniqueproof · cited by 6
- groupCohomology.comp_d₀₁_eqproof · cited by 6
- AddEquiv.funUniqueproof · cited by 5
- ContinuousMultilinearMap.norm_ofSubsingletonproof · cited by 4
- Equiv.funUnique_symm_applystatement and proof · cited by 4