Theorems · Inductive type · algebraic topology

SSet.Subcomplex.PairingCore.RankFunction

{X : SSet} → {A : X.Subcomplex} → A.PairingCore → (α : Type v) → [PartialOrder α] → Type (max u_1 v)

A rank function for h : A.PairingCore is a function from the index type h.ι to a partially ordered type which maps the ancestrality relations to strict inequalities.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Cited by

7 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Quot.sound

Assumes

PartialOrder