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.range_eq_iSup_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) {X : SSet} (φ : c.pt ⟶ X) : Subcomplex.range φ = ⨆ (j : J), Subcomplex.range (CategoryTheory.CategoryStruct.comp (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

theorem SSet.range_eq_iSup_sigma_ι {ι : Type v} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ι) (Type u)] {X : ι → SSet} {Y : SSet} [CategoryTheory.Limits.HasCoproduct X] (f : ∐ X ⟶ Y) : Subcomplex.range f = ⨆ (i : ι), Subcomplex.range (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X i) f)