Commit 2026-03-25 06:04 a317013c

View on Github →

feat(Topology/Category): TopCat is cartesian monoidal (#37097)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Category/TopCat/Basic.lean

added def TopCat.const

added theorem TopCat.const_apply

Created Mathlib/Topology/Category/TopCat/Monoidal.lean

added theorem TopCat.I.ext

added def TopCat.I.homeomorph

added theorem TopCat.I.homeomorph_one

added theorem TopCat.I.homeomorph_symm

added theorem TopCat.I.homeomorph_zero

added def TopCat.I.symm

added theorem TopCat.I.symm_one

added theorem TopCat.I.symm_zero

added def TopCat.I

added theorem TopCat.associator_hom_apply

added theorem TopCat.associator_hom_apply_1

added theorem TopCat.associator_hom_apply_2_1

added theorem TopCat.associator_hom_apply_2_2

added theorem TopCat.associator_inv_apply

added theorem TopCat.associator_inv_apply_1_1

added theorem TopCat.associator_inv_apply_1_2

added theorem TopCat.associator_inv_apply_2

added theorem TopCat.braiding_hom_apply

added theorem TopCat.braiding_inv_apply

added theorem TopCat.leftUnitor_hom_apply

added theorem TopCat.leftUnitor_inv_apply

added theorem TopCat.rightUnitor_hom_apply

added theorem TopCat.rightUnitor_inv_apply

added theorem TopCat.tensor_apply

added theorem TopCat.whiskerLeft_apply

added theorem TopCat.whiskerRight_apply

added theorem TopCat.ι₀_apply

added theorem TopCat.ι₀_comp

added theorem TopCat.ι₀_fst

added theorem TopCat.ι₀_snd

added theorem TopCat.ι₁_apply

added theorem TopCat.ι₁_comp

added theorem TopCat.ι₁_fst

added theorem TopCat.ι₁_snd