Theorems · Definition · algebraic topology

SSet.Subcomplex.PairingCore.WeakRankFunction.recOn

{X : SSet} →
  {A : X.Subcomplex} →
    {h : A.PairingCore} →
      {α : Type v} →
        [inst : PartialOrder α] →
          {motive : h.WeakRankFunction α → Sort u_2} →
            (t : h.WeakRankFunction α) →
              ((rank : h.ι → α) →
                  (lt : ∀ {x y : h.ι}, h.AncestralRel x y → h.dim x = h.dim y → rank x < rank y) →
                    motive { rank := rank, lt := lt }) →
                motive t

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Cited by

0 results in Mathlib

Foundations

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

Assumes

PartialOrder