Finite simplicial sets

A simplicial set is finite (SSet.Finite) if it has finitely many nondegenerate simplices.

class SSet.Finite (X : SSet) : Prop

A simplicial set is finite if it has finitely many nondegenerate simplices.

• finite : Finite X.N

instance SSet.instFiniteElemObjOppositeSimplexCategoryOpMkNonDegenerateOfFinite (X : SSet) [X.Finite] (n : ℕ) : Finite ↑(X.nonDegenerate n)

theorem SSet.finite_of_hasDimensionLT (X : SSet) (d : ℕ) [X.HasDimensionLT d] (h : ∀ i < d, Finite ↑(X.nonDegenerate i)) : X.Finite

theorem SSet.hasDimensionLT_of_finite (X : SSet) [X.Finite] : ∃ (d : ℕ), X.HasDimensionLT d

instance SSet.instFiniteObjOppositeSimplexCategoryOfFinite (X : SSet) [X.Finite] (n : SimplexCategoryᵒᵖ) : Finite (X.obj n)

instance SSet.instFiniteToSSet (X : SSet) [X.Finite] (A : X.Subcomplex) : A.toSSet.Finite

theorem SSet.finite_of_mono {X Y : SSet} [Y.Finite] (f : X ⟶ Y) [hf : CategoryTheory.Mono f] : X.Finite

theorem SSet.finite_of_epi {X Y : SSet} [X.Finite] (f : X ⟶ Y) [hf : CategoryTheory.Epi f] : Y.Finite

theorem SSet.finite_of_iso {X Y : SSet} (e : X ≅ Y) [X.Finite] : Y.Finite

theorem SSet.finite_iff_of_iso {X Y : SSet} (e : X ≅ Y) : X.Finite ↔ Y.Finite

theorem SSet.finite_subcomplex_top_iff (X : SSet) : ⊤.toSSet.Finite ↔ X.Finite

instance SSet.finite_range {X Y : SSet} (f : Y ⟶ X) [Y.Finite] : (Subcomplex.range f).toSSet.Finite

theorem SSet.finite_iSup_iff {X : SSet} {ι : Type u_1} [Finite ι] (A : ι → X.Subcomplex) : (⨆ (i : ι), A i).toSSet.Finite ↔ ∀ (i : ι), (A i).toSSet.Finite