def SimplicialComplex.linkComplex {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (σ : Finset V) (hσ : σ ∈ K.faces) : SimplicialComplex V

The link complex $\mathrm{lk}_K(\sigma)$ of a face $\sigma$ as a simplicial complex: its faces are the nonempty $\tau$ disjoint from $\sigma$ such that $\sigma \cup \tau \in K$.

theorem SimplicialComplex.linkComplex_disjoint {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (σ : Finset V) (hσ : σ ∈ K.faces) (τ : Finset V) (hτ : τ ∈ (K.linkComplex σ hσ).faces) : Disjoint σ τ

Every face $\tau$ of $\mathrm{lk}_K(\sigma)$ is disjoint from $\sigma$.

theorem SimplicialComplex.linkComplex_union_mem {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (σ : Finset V) (hσ : σ ∈ K.faces) (τ : Finset V) (hτ : τ ∈ (K.linkComplex σ hσ).faces) : σ ∪ τ ∈ K.faces

For each face $\tau \in \mathrm{lk}_K(\sigma)$, the union $\sigma \cup \tau$ is a face of $K$.

theorem SimplicialComplex.mem_linkComplex_iff {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (σ : Finset V) (hσ : σ ∈ K.faces) (τ : Finset V) : τ ∈ (K.linkComplex σ hσ).faces ↔ τ.Nonempty ∧ Disjoint σ τ ∧ σ ∪ τ ∈ K.faces

Membership characterisation of $\mathrm{lk}_K(\sigma)$: $\tau$ lies in the link iff $\tau$ is nonempty, disjoint from $\sigma$, and $\sigma \cup \tau$ is a face.

theorem SimplicialComplex.linkComplex_face_mem_faces {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (σ : Finset V) (hσ : σ ∈ K.faces) (τ : Finset V) (hτ : τ ∈ (K.linkComplex σ hσ).faces) : τ ∈ K.faces

Every face of $\mathrm{lk}_K(\sigma)$ is itself a face of $K$.

theorem SimplicialComplex.mem_linkComplex_of_sdiff {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (σ : Finset V) (hσ : σ ∈ K.faces) (w : Finset V) (hw : w ∈ K.faces) (hσw : σ ⊆ w) (hne : (w \ σ).Nonempty) : w \ σ ∈ (K.linkComplex σ hσ).faces

For a face $w$ properly containing $\sigma$, the complement $w \setminus \sigma$ is a face of $\mathrm{lk}_K(\sigma)$.