Theorems · Theorem · category theory
CategoryTheory.CardinalDirectedPoset.exists_mem_propSetWithTop
∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (κ' : Cardinal.{u})
[inst_1 : Fact κ'.IsRegular] (a : ↑J.withTop.obj), ∃ S, J.PropSetWithTop κ' S ∧ a ∈ S- Cited by
- 1 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Top.topproof · cited by 9,680
- 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.someproof · cited by 1,128
- Cardinal.IsRegularstatement and proof · cited by 282
- Classical.arbitraryproof · cited by 161
- PartOrdEmbstatement · cited by 68
- PartOrdEmb.carrierstatement and proof · cited by 61
- PartOrdEmb.isCardinalFilteredstatement · cited by 25
- CategoryTheory.CardinalDirectedPosetstatement and proof · cited by 24
Cited by1
Results whose statement or proof uses this declaration.
- CategoryTheory.CardinalFilteredPoset.exists_mem_propSetWithTopproof · cited by 0