English
Construct a simplicial complex by removing the empty face from a given family of candidate faces, while preserving independence, down-closure, and intersection-compatibility.
Русский
Построим симплициальный комплекс из заданного семейства граней, удалив пустое множество, сохранив независимость, замкнутость по частям и совместимость пересечений.
LaTeX
$$$\\text{faces}(\\mathrm{ofErase}(faces, indep, down\_closed, inter\_subset\_convexHull)) = faces \\setminus \\{\\emptyset\\}$$$
Lean4
/-- Construct a simplicial complex by removing the empty face for you. -/
@[simps]
def ofErase (faces : Set (Finset E)) (indep : ∀ s ∈ faces, AffineIndependent 𝕜 ((↑) : s → E))
(down_closed : ∀ s ∈ faces, ∀ t ⊆ s, t ∈ faces)
(inter_subset_convexHull :
∀ᵉ (s ∈ faces) (t ∈ faces), convexHull 𝕜 ↑s ∩ convexHull 𝕜 ↑t ⊆ convexHull 𝕜 (s ∩ t : Set E)) :
SimplicialComplex 𝕜 E where
faces := faces \ {∅}
empty_notMem h := h.2 (mem_singleton _)
indep hs := indep _ hs.1
down_closed hs hts ht := ⟨down_closed _ hs.1 _ hts, ht⟩
inter_subset_convexHull hs ht := inter_subset_convexHull _ hs.1 _ ht.1
