Theorems · Definition · algebraic topology

SSet.Truncated.Edge.tensor

{X Y : SSet.Truncated 2} →
  {x x' : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })} →
    SSet.Truncated.Edge x x' →
      {y y' : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })} →
        SSet.Truncated.Edge y y' → SSet.Truncated.Edge (x, y) (x', y')

The external product of edges of 2-truncated simplicial sets.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Cited by

16 results in Mathlib

Foundations

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