MulStruct

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/KanComplex/MulStruct.lean

Statistics

Metric	Count
Definitions PtSimplex, MulStruct, map, RelStruct, map	5
Theorems δ_castSucc_castSucc_map, δ_castSucc_castSucc_map_assoc, δ_map_of_gt, δ_map_of_lt, δ_succ_castSucc_map, δ_succ_castSucc_map_assoc, δ_succ_succ_map, δ_succ_succ_map_assoc, δ_castSucc_map, δ_castSucc_map_assoc, δ_map_of_gt, δ_map_of_lt, δ_succ_map, δ_succ_map_assoc	14
Total	19

SSet

Definitions

Name	Category	Theorems
PtSimplex 📖	CompOp	—

SSet.PtSimplex

Definitions

Name	Category	Theorems
MulStruct 📖	CompData	—
RelStruct 📖	CompData	—

SSet.PtSimplex.MulStruct

Definitions

Name	Category	Theorems
map 📖	CompOp	8 math math: δ_map_of_gt, δ_succ_succ_map_assoc, δ_succ_succ_map, δ_succ_castSucc_map, δ_map_of_lt, δ_castSucc_castSucc_map_assoc, δ_succ_castSucc_map_assoc, δ_castSucc_castSucc_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
δ_castSucc_castSucc_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.RelativeMorphism.map SSet.boundary SSet.Subcomplex.ofSimplex SSet.const SSet.Subcomplex.toSSet Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj	—	—
δ_castSucc_castSucc_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.RelativeMorphism.map SSet.boundary SSet.Subcomplex.ofSimplex SSet.const SSet.Subcomplex.toSSet Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_castSucc_castSucc_map
δ_map_of_gt 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.const	—	—
δ_map_of_lt 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.const	—	—
δ_succ_castSucc_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.RelativeMorphism.map SSet.boundary SSet.Subcomplex.ofSimplex SSet.const SSet.Subcomplex.toSSet Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj	—	—
δ_succ_castSucc_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.RelativeMorphism.map SSet.boundary SSet.Subcomplex.ofSimplex SSet.const SSet.Subcomplex.toSSet Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_succ_castSucc_map
δ_succ_succ_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.RelativeMorphism.map SSet.boundary SSet.Subcomplex.ofSimplex SSet.const SSet.Subcomplex.toSSet Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj	—	—
δ_succ_succ_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.RelativeMorphism.map SSet.boundary SSet.Subcomplex.ofSimplex SSet.const SSet.Subcomplex.toSSet Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_succ_succ_map

SSet.PtSimplex.RelStruct

Definitions

Name	Category	Theorems
map 📖	CompOp	6 math math: δ_map_of_lt, δ_castSucc_map, δ_castSucc_map_assoc, δ_succ_map, δ_map_of_gt, δ_succ_map_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
δ_castSucc_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.RelativeMorphism.map SSet.boundary SSet.Subcomplex.ofSimplex SSet.const SSet.Subcomplex.toSSet Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj	—	—
δ_castSucc_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.RelativeMorphism.map SSet.boundary SSet.Subcomplex.ofSimplex SSet.const SSet.Subcomplex.toSSet Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_castSucc_map
δ_map_of_gt 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.const	—	—
δ_map_of_lt 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.const	—	—
δ_succ_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.RelativeMorphism.map SSet.boundary SSet.Subcomplex.ofSimplex SSet.const SSet.Subcomplex.toSSet Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj	—	—
δ_succ_map_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp SSet CategoryTheory.Category.toCategoryStruct SSet.largeCategory CategoryTheory.Functor.obj SimplexCategory SimplexCategory.smallCategory SSet.stdSimplex CategoryTheory.CosimplicialObject.δ map SSet.RelativeMorphism.map SSet.boundary SSet.Subcomplex.ofSimplex SSet.const SSet.Subcomplex.toSSet Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Set Set.instMembership CategoryTheory.Subfunctor.obj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δ_succ_map

---

← Back to Index