MorphismProperty

📁 Source: Mathlib/AlgebraicTopology/SimplexCategory/MorphismProperty.lean

Statistics

Metric	Count
Definitions	0
Theorems morphismProperty_eq_top, morphismProperty_eq_top	2
Total	2

SimplexCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
morphismProperty_eq_top 📖	mathematical	δ σ	Top.top CategoryTheory.MorphismProperty SimplexCategory CategoryTheory.Category.toCategoryStruct smallCategory BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	Truncated.morphismProperty_eq_top CategoryTheory.MorphismProperty.IsMultiplicative.instInverseImage CategoryTheory.MorphismProperty.ext

SimplexCategory.Truncated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
morphismProperty_eq_top 📖	mathematical	SimplexCategory SimplexCategory.smallCategory SimplexCategory.len δ σ	Top.top CategoryTheory.MorphismProperty SimplexCategory.Truncated CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	CategoryTheory.MorphismProperty.ext CategoryTheory.MorphismProperty.id_mem CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities Hom.ext OrderHom.ext CategoryTheory.ObjectProperty.hom_ext SimplexCategory.eq_id_of_epi le_antisymm SimplexCategory.len_le_of_mono SimplexCategory.mono_iff_injective SimplexCategory.len_le_of_epi SimplexCategory.epi_iff_surjective Function.injective_of_subsingleton SimplexCategory.eq_σ_comp_of_not_injective CategoryTheory.InducedCategory.hom_ext CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition SimplexCategory.eq_comp_δ_of_not_surjective

---

← Back to Index