Theorems · Definition · algebraic topology

SSet.Subcomplex.Pairing.WeakRankFunction.casesOn

{X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {α : Type v} →
        [inst : PartialOrder α] →
          {motive : P.WeakRankFunction α → Sort u_1} →
            (t : P.WeakRankFunction α) →
              ((rank : ↑P.II → α) →
                  (lt : ∀ {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim = (↑y).dim → 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