Theorems · Theorem · category theory
FintypeCat.uSwitchEquiv_symm_naturality
∀ {X Y : FintypeCat} (f : X ⟶ Y) (x : X.obj),
(CategoryTheory.ConcreteCategory.hom (FintypeCat.uSwitch.map f)) (X.uSwitchEquiv.symm x) =
Y.uSwitchEquiv.symm ((CategoryTheory.ConcreteCategory.hom f) x)- Defined in
- Mathlib.CategoryTheory.FintypeCat
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functor.objstatement · cited by 19,642
- CategoryTheory.Functor.mapstatement · cited by 8,698
- Equivstatement · cited by 8,337
- CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
- Equiv.symmstatement and proof · cited by 3,681
- Finitestatement and proof · cited by 3,029
- CategoryTheory.ObjectProperty.FullSubcategory.objstatement and proof · cited by 1,316
- TypeCat.Funstatement · cited by 1,307
- CategoryTheory.ObjectProperty.FullSubcategorystatement and proof · cited by 726
- Equiv.apply_symm_applyproof · cited by 346
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.