Theorems · Definition · category theory
TopologicalSpace.Opens.infLELeft
{X : TopCat} → (U V : TopologicalSpace.Opens ↑X) → U ⊓ V ⟶ UThe inclusion U ⊓ V ⟶ U as a morphism in the category of open sets.
- Defined in
- Mathlib.Topology.Category.TopCat.Opens
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement · cited by 32,603
- TopCat.carrierstatement and proof · cited by 3,184
- TopologicalSpace.Opensstatement and proof · cited by 2,040
- TopCatstatement and proof · cited by 1,889
- LE.le.homproof · cited by 30
Cited by15
Results whose statement or proof uses this declaration.
- TopCat.Presheaf.IsCompatibleproof · cited by 10
- TopCat.Presheaf.SheafConditionEqualizerProducts.leftResproof · cited by 7
- TopCat.Sheaf.eq_of_locally_eqproof · cited by 4
- TopCat.Presheaf.objPairwiseOfFamilyproof · cited by 3
- AlgebraicGeometry.RingedSpace.isUnit_res_of_isUnit_germproof · cited by 1
- TopCat.Sheaf.IsFlasque.structured_arrows_elements_sheaf_chains_boundedproof · cited by 1
- TopCat.Presheaf.SheafConditionEqualizerProducts.wproof · cited by 1
- TopCat.Presheaf.app_surjective_of_injective_of_locally_surjectiveproof · cited by 1
- AlgebraicGeometry.RingedSpace.isUnit_of_isUnit_germproof · cited by 1
- TopCat.Presheaf.stalkToFiber_injectiveproof · cited by 0
- TopCat.PrelocalPredicate.sheafify_inductionOn₂'proof · cited by 0