Finite colimits of finite simplicial sets are finite

theorem SSet.iSup_range_eq_top_of_isColimit {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] [CategoryTheory.Limits.HasColimitsOfShape J (Type u)] {F : CategoryTheory.Functor J SSet} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) : ⨆ (j : J), Subcomplex.range (c.ι.app j) = ⊤

theorem SSet.hasDimensionLT_of_isColimit {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] [CategoryTheory.Limits.HasColimitsOfShape J (Type u)] {F : CategoryTheory.Functor J SSet} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) {n : ℕ} (h : ∀ (j : J), (F.obj j).HasDimensionLT n) : c.pt.HasDimensionLT n

theorem SSet.finite_of_isColimit {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] [CategoryTheory.Limits.HasColimitsOfShape J (Type u)] {F : CategoryTheory.Functor J SSet} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c) [Finite J] (h : ∀ (j : J), (F.obj j).Finite) : c.pt.Finite

instance SSet.instFiniteInitial : (⊥_ SSet).Finite

instance SSet.instFiniteCoprod (X Y : SSet) [X.Finite] [Y.Finite] : (X ⨿ Y).Finite

instance SSet.instFiniteSigmaObjOfFinite {ι : Type v} [Finite ι] (X : ι → SSet) [CategoryTheory.Limits.HasCoproduct X] [∀ (j : ι), (X j).Finite] : (∐ X).Finite