HasCardinalLT

📁 Source: Mathlib/CategoryTheory/ObjectProperty/HasCardinalLT.lean

Statistics

Metric	Count
Definitions HasCardinalLT	1
Theorems iSup, sup, hasCardinalLT_subtype_ofObj	3
Total	4

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
HasCardinalLT 📖	MathDef	2 math math: CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.hP, hasCardinalLT_subtype_ofObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCardinalLT_subtype_ofObj 📖	mathematical	HasCardinalLT	HasCardinalLT ofObj CategoryTheory.Category.toCategoryStruct	—	HasCardinalLT.of_surjective

CategoryTheory.ObjectProperty.HasCardinalLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iSup 📖	mathematical	CategoryTheory.ObjectProperty.HasCardinalLT HasCardinalLT	iSup CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.supSet ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Prop.instCompleteLinearOrder	—	hasCardinalLT_subtype_iSup
sup 📖	mathematical	CategoryTheory.ObjectProperty.HasCardinalLT Cardinal Cardinal.instLE Cardinal.aleph0	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instMaxForall_mathlib SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Prop.instCompleteLinearOrder	—	hasCardinalLT_union

---

← Back to Index