SSet.iSup_subcomplexOfSimplex_prod_eq_top

∀ (X₁ X₂ : SSet), ⨆ x₁, ⨆ x₂, (SSet.Subcomplex.ofSimplex x₁.simplex).prod (SSet.Subcomplex.ofSimplex x₂.simplex) = ⊤

Defined in: Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
Cited by: 1 results in Mathlib
Foundations: Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Functor.objproof · cited by 19,642
Top.topstatement and proof · cited by 9,680
Oppositestatement and proof · cited by 8,081
CategoryTheory.MonoidalCategoryStruct.tensorObjstatement and proof · cited by 3,106
Set.iUnionproof · cited by 2,483
iSupstatement and proof · cited by 2,415
Set.extproof · cited by 2,266
SimplexCategorystatement and proof · cited by 2,204
SSetstatement and proof · cited by 1,283
SSet.Subcomplexstatement · cited by 461
CategoryTheory.Subfunctor.objproof · cited by 227
SSet.N.toSstatement and proof · cited by 171

Results whose statement or proof uses this declaration.