degenerate — Mathlib

English

An n-simplex of a simplicial set X is degenerate if it lies in the image of X.map f.op for some f: [n] → [m] with m < n.

Русский

Дегенерируемый n-симплекс множества X есть образ X.map f.op для некоторого f: [n] → [m] с m < n.

LaTeX

$$$ X\text{degenerate}(n) = \{ x \in X_n : \exists m

Lean4

/-- An `n`-simplex of a simplicial set `X` is degenerate if it is in the range
of `X.map f.op` for some morphism `f : [n] ⟶ [m]` with `m < n`. -/
def degenerate (n : ℕ) : Set (X _⦋n⦌) :=
  setOf (fun x ↦ ∃ (m : ℕ) (_ : m < n) (f : ⦋n⦌ ⟶ ⦋m⦌), x ∈ Set.range (X.map f.op))

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