Theorems · Definition · algebraic topology

SSet.Truncated.Edge.CompStruct.map

{X Y : SSet.Truncated 2} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })} →
    {e₀₁ : SSet.Truncated.Edge x₀ x₁} →
      {e₁₂ : SSet.Truncated.Edge x₁ x₂} →
        {e₀₂ : SSet.Truncated.Edge x₀ x₂} →
          e₀₁.CompStruct e₁₂ e₀₂ → (f : X ⟶ Y) → (e₀₁.map f).CompStruct (e₁₂.map f) (e₀₂.map f)

The image of a Edge.CompStruct by a morphism of 2-truncated simplicial sets.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Cited by

1 results in Mathlib

Foundations

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