Theorems · Definition · algebraic topology

SSet.Subcomplex.Pairing.WeakRankFunction.mk.noConfusion

{X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {α : Type v} →
        {inst : PartialOrder α} →
          {P_1 : Sort u_1} →
            {rank : ↑P.II → α} →
              {lt : ∀ {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim = (↑y).dim → rank x < rank y} →
                {rank' : ↑P.II → α} →
                  {lt' : ∀ {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim = (↑y).dim → rank' x < rank' y} →
                    { rank := rank, lt := lt } = { rank := rank', lt := lt' } → (rank ≍ rank' → P_1) → P_1

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Cited by

1 results in Mathlib

Foundations

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