Mathlib Map

Theorems · Definition · category theory

Opposite.casesOn

{α : Sort u} → {motive : αᵒᵖ → Sort u_1} → (t : αᵒᵖ) → ((unop : α) → motive (Opposite.op unop)) → motive t
Defined in
Mathlib.Data.Opposite
Cited by
37 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

SSet.Subcomplex.le_iff_contains_nonDegenerate · cited by 7Subcomplex.le_iff_contain…CategoryTheory.GrothendieckTopology.Point.presheafFiber_hom_ext · cited by 5Point.presheafFiber_hom_e…SSet.S.equivElements · cited by 5S.equivElementsAlgebraicGeometry.PresheafedSpace.stalkMap.comp · cited by 4stalkMap.compCategoryTheory.Presheaf.isSeparating · cited by 3Presheaf.isSeparatingSSet.Truncated.IsStrictSegal.hom_ext · cited by 3IsStrictSegal.hom_extSSet.stdSimplex.face_eq_ofSimplex · cited by 3stdSimplex.face_eq_ofSimp…AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq · cited by 2AlgebraicGeometry.isIso_p…TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types · cited by 2Presheaf.isSheaf_iff_isSh…TopCat.Sheaf.interUnionPullbackConeLift · cited by 2Sheaf.interUnionPullbackC…TopCat.Presheaf.pullback_obj_obj_ext · cited by 2Presheaf.pullback_obj_obj…CategoryTheory.ObjectProperty.op_isoClosure · cited by 2ObjectProperty.op_isoClos…CategoryTheory.PresheafHom.isAmalgamation_iff · cited by 1PresheafHom.isAmalgamatio…CategoryTheory.Functor.IsDense.of_fullyFaithful_restrictedULiftYoneda · cited by 1IsDense.of_fullyFaithful_…SSet.relativeCellComplexOfMono.sup_range_r_range_b · cited by 1relativeCellComplexOfMono…Opposite · cited by 8081OppositeOpposite.casesOnCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Oppositestatement and proof · cited by 8,081

Cited by42

Results whose statement or proof uses this declaration.