Theorems · Definition · algebraic topology

SSet.Edge

{X : SSet} → X.obj (Opposite.op { len := 0 }) → X.obj (Opposite.op { len := 0 }) → Type u

In a simplicial set, an edge from a vertex x₀ to x₁ is a 1-simplex with prescribed 0-dimensional faces.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.CompStruct

Cited by

55 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound