English
Given a simplicial complex K and a collection of faces F which are a subset of K.faces, with a down-closed condition, you can form a subcomplex whose faces are exactly F.
Русский
Заданый подкомплекс, получаемый из семейства граней F, являющегося подмножеством граней K, и нижне-замкнутости, образует соподчиненный комплекс.
LaTeX
$$$\\mathrm{ofSubcomplex}(K, faces, subset, down\_closed)$$$
Lean4
/-- Construct a simplicial complex as a subset of a given simplicial complex. -/
@[simps]
def ofSubcomplex (K : SimplicialComplex 𝕜 E) (faces : Set (Finset E)) (subset : faces ⊆ K.faces)
(down_closed : ∀ {s t}, s ∈ faces → t ⊆ s → t ∈ faces) : SimplicialComplex 𝕜 E :=
{ faces
empty_notMem := fun h => K.empty_notMem (subset h)
indep := fun hs => K.indep (subset hs)
down_closed := fun hs hts _ => down_closed hs hts
inter_subset_convexHull := fun hs ht => K.inter_subset_convexHull (subset hs) (subset ht) }
