Theorems · Definition · category theory
TopologicalSpace.OpenNhds.inclusion
{X : TopCat} → (x : ↑X) → CategoryTheory.Functor (TopologicalSpace.OpenNhds x) (TopologicalSpace.Opens ↑X)The inclusion functor from open neighbourhoods of x
to open sets in the ambient topological space.
- Cited by
- 44 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functorstatement · cited by 16,252
- TopCat.carrierstatement and proof · cited by 3,184
- TopologicalSpace.Opensstatement · cited by 2,040
- TopCatstatement and proof · cited by 1,889
- Monotone.functorproof · cited by 66
- TopologicalSpace.OpenNhdsstatement · cited by 61
Cited by63
Results whose statement or proof uses this declaration.
- TopCat.Presheaf.germproof · cited by 208
- TopCat.Presheaf.stalkSpecializesproof · cited by 51
- TopCat.Presheaf.stalkFunctorproof · cited by 37
- TopCat.Presheaf.germ_resproof · cited by 19
- TopCat.Presheaf.exists_germ_eqproof · cited by 14
- smoothSheafCommRing.evalHomproof · cited by 13
- smoothSheafCommRing.forgetStalkproof · cited by 13
- TopCat.Presheaf.stalkPushforwardproof · cited by 12
- TopCat.Presheaf.germ_stalkSpecializesproof · cited by 10
- TopCat.Presheaf.germ_eqproof · cited by 9
- TopCat.Presheaf.germ_res'proof · cited by 8
- AlgebraicGeometry.PresheafedSpace.restrictStalkIsoproof · cited by 7