A binary product of finite simplicial sets is finite

If X₁ and X₂ are respectively of dimensions ≤ d₁ and ≤ d₂, then X₁ ⊗ X₂ has dimension ≤ d₁ + d₂.

We also show that if X₁ and X₂ are finite, then X₁ ⊗ X₂ is also finite.

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

theorem SSet.Subcomplex.ofSimplexProd_eq_range {X₁ X₂ : SSet} {p q : ℕ} (x₁ : X₁.obj (Opposite.op { len := p })) (x₂ : X₂.obj (Opposite.op { len := q })) : (ofSimplex x₁).prod (ofSimplex x₂) = range (CategoryTheory.MonoidalCategoryStruct.tensorHom (yonedaEquiv.symm x₁) (yonedaEquiv.symm x₂))

theorem SSet.hasDimensionLT_prod (X₁ X₂ : SSet) (d₁ d₂ : ℕ) [X₁.HasDimensionLT d₁] [X₂.HasDimensionLT d₂] (n : ℕ) (hn : d₁ + d₂ ≤ n + 1 := by lia) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂).HasDimensionLT n

theorem SSet.hasDimensionLE_prod (X₁ X₂ : SSet) (d₁ d₂ : ℕ) [X₁.HasDimensionLE d₁] [X₂.HasDimensionLE d₂] (n : ℕ) (hn : d₁ + d₂ ≤ n := by lia) : (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂).HasDimensionLE n

instance SSet.instHasDimensionLTTensorObjHAddNat {X₁ X₂ : SSet} (d₁ d₂ : ℕ) [X₁.HasDimensionLT d₁] [X₂.HasDimensionLT d₂] : (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂).HasDimensionLT (d₁ + d₂)

instance SSet.instHasDimensionLETensorObjHAddNat {X₁ X₂ : SSet} (d₁ d₂ : ℕ) [X₁.HasDimensionLE d₁] [X₂.HasDimensionLE d₂] : (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂).HasDimensionLE (d₁ + d₂)

instance SSet.instFiniteTensorObj {X₁ X₂ : SSet} [X₁.Finite] [X₂.Finite] : (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂).Finite

theorem SSet.finite_of_isPullback {X₁ X₂ X₃ X₄ : SSet} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} (sq : CategoryTheory.IsPullback t l r b) [X₂.Finite] [X₃.Finite] : X₁.Finite

instance SSet.instFinitePullback {X₂ X₃ X₄ : SSet} [X₂.Finite] [X₃.Finite] (r : X₂ ⟶ X₄) (b : X₃ ⟶ X₄) : (CategoryTheory.Limits.pullback r b).Finite