Theorems · Definition · category theory
CategoryTheory.discreteEquiv
{α : Type u₁} → CategoryTheory.Discrete α ≃ αDiscrete α is equivalent to the original type α.
- Defined in
- Mathlib.CategoryTheory.Discrete.Basic
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses propext
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
- CategoryTheory.Discretestatement · cited by 2,447
- CategoryTheory.Discrete.asproof · cited by 269
Cited by8
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.sigmaOpenCoverproof · cited by 4
- CategoryTheory.Discrete.as_bijectiveproof · cited by 1
- CategoryTheory.Discrete.existsproof · cited by 0
- CategoryTheory.Discrete.forallproof · cited by 0
- CategoryTheory.Limits.CompleteLattice.finite_coproduct_eq_finset_supproof · cited by 0
- CategoryTheory.Limits.CompleteLattice.finite_product_eq_finset_infproof · cited by 0
- CategoryTheory.discreteEquiv_applystatement and proof · cited by 0
- CategoryTheory.discreteEquiv_symm_apply_asstatement and proof · cited by 0