The opposite of a subcomplex

def SSet.Subcomplex.op {X : SSet} (A : X.Subcomplex) : X.op.Subcomplex

The opposite of subcomplex, as a subcomplex of the opposite simplicial set.

Equations

• A.op = { obj := A.obj, map := ⋯ }

theorem SSet.Subcomplex.mem_op_obj_iff {X : SSet} (A : X.Subcomplex) {d : SimplexCategoryᵒᵖ} (x : X.op.obj d) : x ∈ A.op.obj d ↔ opObjEquiv x ∈ A.obj d