ofSimplex — Mathlib

English

The subcomplex generated by a simplex x is the section subpresheaf generated by x.

Русский

Подкомплекс, порожденный simplex x, является подпредпосылкой секции, порожденной x.

LaTeX

$$$$ \text{ofSimplex } x = \text{Subpresheaf.ofSection } x $$$$

Lean4

/-- The subcomplex of a simplicial set that is generated by a simplex. -/
abbrev ofSimplex {n : ℕ} (x : X _⦋n⦌) : X.Subcomplex :=
  Subpresheaf.ofSection x

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