Theorems · Theorem · algebraic topology

SSet.Subcomplex.Pairing.WeakRankFunction.mk.sizeOf_spec

∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] [inst_1 : SizeOf α]
  (rank : ↑P.II → α) (lt : ∀ {x y : ↑P.II}, P.AncestralRel x y → (↑x).dim = (↑y).dim → rank x < rank y),
  sizeOf { rank := rank, lt := lt } = 1

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Cited by

0 results in Mathlib

Foundations

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

Assumes

PartialOrderSizeOf