Theorems · Definition · algebraic topology

SSet.Subcomplex.Pairing.RankFunction.relativeCellComplex

{X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          (f : P.RankFunction ι) →
            [inst_1 : P.IsProper] →
              [inst_2 : SuccOrder ι] →
                [inst_3 : OrderBot ι] →
                  [NoMaxOrder ι] → [inst_5 : WellFoundedLT ι] → HomotopicalAlgebra.RelativeCellComplex f.basicCell A.ι

Given a rank function f : P.RankFunction ι for a proper pairing P of a subcomplex A of simplicial set X, the inclusion A.ι is a relative cell complex with basic cells given by horn inclusions.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderSSet.Subcomplex.Pairing.IsProperSuccOrderOrderBotNoMaxOrderWellFoundedLT