Theorems · Theorem · category theory
CategoryTheory.CardinalDirectedPoset.propSetWithTop_pair
∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J : CategoryTheory.CardinalDirectedPoset κ} (κ' : Cardinal.{u})
[inst_1 : Fact κ'.IsRegular] (j : ↑J.obj), J.PropSetWithTop κ' {↑j, ⊤}- Cited by
- 2 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Top.topstatement and proof · cited by 9,680
- Set.Elemproof · cited by 7,166
- WithTopstatement · cited by 3,754
- Factstatement and proof · cited by 2,726
- Cardinalstatement and proof · cited by 2,598
- CategoryTheory.ObjectProperty.FullSubcategory.objstatement and proof · cited by 1,316
- WithTop.somestatement and proof · cited by 1,128
- Fact.outproof · cited by 328
- Cardinal.IsRegularstatement and proof · cited by 282
- PartOrdEmbstatement · cited by 68
- PartOrdEmb.carrierstatement and proof · cited by 61
Cited by2
Results whose statement or proof uses this declaration.
- CategoryTheory.CardinalDirectedPoset.exists_mem_propSetWithTopproof · cited by 1
- CategoryTheory.CardinalFilteredPoset.propSetWithTop_pairproof · cited by 0