Monoidal

📁 Source: Mathlib/Topology/Category/TopCat/Monoidal.lean

Statistics

Metric	Count
Definitions I, homeomorph, instOfNatCarrierOfNatNat, instOfNatCarrierOfNatNat_1, instBraidedCategory, instCartesianMonoidalCategory, ι₀, ι₁	8
Theorems ext, ext_iff, homeomorph_one, homeomorph_symm, homeomorph_zero, symm_one, symm_zero, associator_hom_apply, associator_hom_apply_1, associator_hom_apply_2_1, associator_hom_apply_2_2, associator_inv_apply, associator_inv_apply_1_1, associator_inv_apply_1_2, associator_inv_apply_2, braiding_hom_apply, braiding_inv_apply, instLocallyCompactSpaceCarrierI, leftUnitor_hom_apply, leftUnitor_inv_apply, lift_apply, rightUnitor_hom_apply, rightUnitor_inv_apply, tensor_apply, whiskerLeft_apply, whiskerRight_apply, ι₀_apply, ι₀_comp, ι₀_comp_assoc, ι₀_fst, ι₀_fst_assoc, ι₀_snd, ι₀_snd_assoc, ι₁_apply, ι₁_comp, ι₁_comp_assoc, ι₁_fst, ι₁_fst_assoc, ι₁_snd, ι₁_snd_assoc	40
Total	48

TopCat

Definitions

Name	Category	Theorems
I 📖	CompOp	33 math math: ι₁_comp_assoc, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ, SSet.stdSimplex.δ_zero_toSSetObjI, I.homeomorph_one, Homotopy.ι₁_h, SSet.stdSimplex.toSSetObj_app_const_zero, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assoc, I.symm_one, I.homeomorph_zero, ι₀_fst, I.ext_iff, Homotopy.ι₀_h_assoc, ι₀_comp_assoc, SSet.stdSimplex.δ_one_toSSetObjI, ι₁_fst, ι₁_apply, ι₀_snd_assoc, instLocallyCompactSpaceCarrierI, ι₀_comp, ι₀_apply, I.symm_zero, ι₀_snd, ι₀_fst_assoc, ι₁_fst_assoc, ι₁_snd_assoc, ι₁_comp, I.homeomorph_symm, ι₁_snd, Homotopy.ι₀_h, SSet.stdSimplex.toSSetObj_app_const_one, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ, Homotopy.ι₁_h_assoc, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assoc
instBraidedCategory 📖	CompOp	2 math math: braiding_inv_apply, braiding_hom_apply
instCartesianMonoidalCategory 📖	CompOp	40 math math: ι₁_comp_assoc, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ, braiding_inv_apply, associator_hom_apply_2_2, braiding_hom_apply, associator_inv_apply_2, rightUnitor_inv_apply, associator_inv_apply_1_2, associator_inv_apply_1_1, Homotopy.ι₁_h, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assoc, ι₀_fst, Homotopy.ι₀_h_assoc, associator_hom_apply_2_1, leftUnitor_inv_apply, ι₀_comp_assoc, ι₁_fst, leftUnitor_hom_apply, ι₁_apply, ι₀_snd_assoc, rightUnitor_hom_apply, ι₀_comp, lift_apply, tensor_apply, ι₀_apply, whiskerRight_apply, ι₀_snd, ι₀_fst_assoc, ι₁_fst_assoc, ι₁_snd_assoc, ι₁_comp, associator_hom_apply_1, ι₁_snd, Homotopy.ι₀_h, associator_hom_apply, whiskerLeft_apply, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ, associator_inv_apply, Homotopy.ι₁_h_assoc, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assoc
ι₀ 📖	CompOp	11 math math: SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assoc, ι₀_fst, Homotopy.ι₀_h_assoc, ι₀_comp_assoc, ι₀_snd_assoc, ι₀_comp, ι₀_apply, ι₀_snd, ι₀_fst_assoc, Homotopy.ι₀_h, SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ
ι₁ 📖	CompOp	11 math math: ι₁_comp_assoc, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ, Homotopy.ι₁_h, ι₁_fst, ι₁_apply, ι₁_fst_assoc, ι₁_snd_assoc, ι₁_comp, ι₁_snd, Homotopy.ι₁_h_assoc, SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	—
associator_hom_apply_1 📖	mathematical	—	carrier CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	—
associator_hom_apply_2_1 📖	mathematical	—	carrier CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	—
associator_hom_apply_2_2 📖	mathematical	—	carrier CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	—
associator_inv_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator	—	—
associator_inv_apply_1_1 📖	mathematical	—	carrier CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator	—	—
associator_inv_apply_1_2 📖	mathematical	—	carrier CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator	—	—
associator_inv_apply_2 📖	mathematical	—	carrier CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator	—	—
braiding_hom_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding instBraidedCategory	—	—
braiding_inv_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding instBraidedCategory	—	—
instLocallyCompactSpaceCarrierI 📖	mathematical	—	LocallyCompactSpace carrier I str	—	—
leftUnitor_hom_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
leftUnitor_inv_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
lift_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.CartesianMonoidalCategory.lift	—	—
rightUnitor_hom_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	—
rightUnitor_inv_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	—
tensor_apply 📖	mathematical	—	DFunLike.coe ContinuousMap carrier CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory str ContinuousMap.instFunLike Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ConcreteCategory.hom instConcreteCategoryContinuousMapCarrier	—	—
whiskerLeft_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
whiskerRight_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
ι₀_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier ι₀ I.instOfNatCarrierOfNatNat	—	—
ι₀_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I ι₀ CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
ι₀_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I ι₀ CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₀_comp
ι₀_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I ι₀ CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.CategoryStruct.id	—	—
ι₀_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I ι₀ CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ι₀_fst
ι₀_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I ι₀ CategoryTheory.SemiCartesianMonoidalCategory.snd const carrier I.instOfNatCarrierOfNatNat	—	—
ι₀_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I ι₀ CategoryTheory.SemiCartesianMonoidalCategory.snd const carrier I.instOfNatCarrierOfNatNat	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₀_snd
ι₁_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.MonoidalCategoryStruct.tensorObj TopCat instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I carrier CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier ι₁ I.instOfNatCarrierOfNatNat_1	—	—
ι₁_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I ι₁ CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
ι₁_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I ι₁ CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₁_comp
ι₁_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I ι₁ CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.CategoryStruct.id	—	—
ι₁_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I ι₁ CategoryTheory.SemiCartesianMonoidalCategory.fst	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' ι₁_fst
ι₁_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I ι₁ CategoryTheory.SemiCartesianMonoidalCategory.snd const carrier I.instOfNatCarrierOfNatNat_1	—	—
ι₁_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp TopCat CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instCartesianMonoidalCategory I ι₁ CategoryTheory.SemiCartesianMonoidalCategory.snd const carrier I.instOfNatCarrierOfNatNat_1	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι₁_snd

TopCat.I

Definitions

Name	Category	Theorems
homeomorph 📖	CompOp	4 math math: homeomorph_one, homeomorph_zero, ext_iff, homeomorph_symm
instOfNatCarrierOfNatNat 📖	CompOp	8 math math: SSet.stdSimplex.toSSetObj_app_const_zero, symm_one, homeomorph_zero, SSet.stdSimplex.δ_one_toSSetObjI, TopCat.ι₀_snd_assoc, TopCat.ι₀_apply, symm_zero, TopCat.ι₀_snd
instOfNatCarrierOfNatNat_1 📖	CompOp	8 math math: SSet.stdSimplex.δ_zero_toSSetObjI, homeomorph_one, symm_one, TopCat.ι₁_apply, symm_zero, TopCat.ι₁_snd_assoc, TopCat.ι₁_snd, SSet.stdSimplex.toSSetObj_app_const_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	DFunLike.coe Homeomorph TopCat.carrier TopCat.I Set.Elem Real unitInterval TopCat.str instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike homeomorph	—	—	Homeomorph.injective
ext_iff 📖	mathematical	—	DFunLike.coe Homeomorph TopCat.carrier TopCat.I Set.Elem Real unitInterval TopCat.str instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike homeomorph	—	ext
homeomorph_one 📖	mathematical	—	DFunLike.coe Homeomorph TopCat.carrier TopCat.I Set.Elem Real unitInterval TopCat.str instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike homeomorph instOfNatCarrierOfNatNat_1 Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing Homeomorph.apply_symm_apply
homeomorph_symm 📖	mathematical	—	DFunLike.coe Homeomorph TopCat.carrier TopCat.I Set.Elem Real unitInterval TopCat.str instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike homeomorph CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier symm unitInterval.symm	—	—
homeomorph_zero 📖	mathematical	—	DFunLike.coe Homeomorph TopCat.carrier TopCat.I Set.Elem Real unitInterval TopCat.str instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike homeomorph instOfNatCarrierOfNatNat Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing Homeomorph.apply_symm_apply
symm_one 📖	mathematical	—	DFunLike.coe TopCat.I TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier symm instOfNatCarrierOfNatNat_1 instOfNatCarrierOfNatNat	—	ext Real.instIsOrderedRing homeomorph_one unitInterval.symm_one homeomorph_zero
symm_zero 📖	mathematical	—	DFunLike.coe TopCat.I TopCat.carrier CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier symm instOfNatCarrierOfNatNat instOfNatCarrierOfNatNat_1	—	ext Real.instIsOrderedRing homeomorph_zero unitInterval.symm_zero homeomorph_one

---

← Back to Index