Theorems · Theorem · algebraic topology

SSet.relativeCellComplexOfMono.Cell.mem_skeletonOfMono_obj_iff

∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : SSet.relativeCellComplexOfMono.Cell i d) {d' : ℕ},
  c.simplex ∈ ((SSet.skeletonOfMono i) d').obj (Opposite.op { len := d }) ↔
    c.simplex ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d }))) ∨ d < d'

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Cited by

0 results in Mathlib

Foundations

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