face — Mathlib

English

Given a Finset S of vertices of Δ[n], the corresponding face is the subcomplex of Δ[n] consisting of faces whose vertex set lies in S.

Русский

Для Finset S вершин Δ[n], соответствующая грань есть подподслой Δ[n], состоящий из граней, вершины которых лежат в S.

LaTeX

$$face(S) : (Δ[n] : SSet).Subcomplex$$

Lean4

/-- Given `S : Finset (Fin (n + 1))`, this is the corresponding face of `Δ[n]`,
as a subcomplex. -/
@[simps -isSimp obj]
def face {n : ℕ} (S : Finset (Fin (n + 1))) : (Δ[n] : SSet.{u}).Subcomplex
    where
  obj U := setOf (fun f ↦ Finset.image (objEquiv f).toOrderHom ⊤ ≤ S)
  map {U V} i := by aesop

Похожие утверждения