Theorems · Definition · algebraic topology

SSet.Edge.mk

{X : SSet} →
  {x₀ x₁ : X.obj (Opposite.op { len := 0 })} →
    (edge : X.obj (Opposite.op { len := 1 })) →
      autoParam ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 1)) edge = x₀) _auto_31✝ →
        autoParam ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) edge = x₁) _auto_33✝ →
          SSet.Edge x₀ x₁

Constructor for edges in a simplicial set.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.CompStruct

Cited by

4 results in Mathlib

Foundations

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