Basic

📁 Source: Mathlib/Topology/Homotopy/TopCat/Basic.lean

Statistics

Metric	Count
Definitions h	1
Theorems ι₀_h, ι₀_h_assoc, ι₁_h, ι₁_h_assoc	4
Total	5

TopCat.Homotopy

Definitions

Name	Category	Theorems
h 📖	CompOp	4 math math: ι₁_h, ι₀_h_assoc, ι₀_h, ι₁_h_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ι₀_h 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory TopCat.instCartesianMonoidalCategory TopCat.I TopCat.ι₀ h	—	TopCat.ext ContinuousMap.Homotopy.map_zero_left
ι₀_h_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory TopCat.instCartesianMonoidalCategory TopCat.I TopCat.ι₀ h	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₀_h
ι₁_h 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory TopCat.instCartesianMonoidalCategory TopCat.I TopCat.ι₁ h	—	TopCat.ext ContinuousMap.Homotopy.map_one_left
ι₁_h_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct TopCat.instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory TopCat.instCartesianMonoidalCategory TopCat.I TopCat.ι₁ h	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₁_h

---

← Back to Index