Theorems · Inductive type · algebraic topology

SSet.Subcomplex.PairingCore.WeakRankFunction

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

A weak rank function h : A.PairingCore is a function from the index type h.ι to a partially ordered type which maps an ancestrality relation between indices of the same dimension to a strict inequality.

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