HasCardinalLT

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

Statistics

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

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
HasCardinalLT 📖	MathDef	2 math math: hasCardinalLT_ofHoms, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.hW

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCardinalLT_ofHoms 📖	mathematical	HasCardinalLT	HasCardinalLT ofHoms	—	HasCardinalLT.of_surjective ofHoms_iff mem_toSet_iff

CategoryTheory.MorphismProperty.HasCardinalLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iSup 📖	mathematical	CategoryTheory.MorphismProperty.HasCardinalLT HasCardinalLT	iSup CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	CategoryTheory.MorphismProperty.toSet_iSup hasCardinalLT_iUnion
sup 📖	mathematical	CategoryTheory.MorphismProperty.HasCardinalLT Cardinal Cardinal.instLE Cardinal.aleph0	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	CategoryTheory.MorphismProperty.toSet_max hasCardinalLT_union

---

← Back to Index