Theorems · Theorem · algebraic topology

SSet.Subcomplex.PairingCore.WeakRankFunction.mk.inj

∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} {inst : PartialOrder α} {rank : h.ι → α}
  {lt : ∀ {x y : h.ι}, h.AncestralRel x y → h.dim x = h.dim y → rank x < rank y} {rank_1 : h.ι → α}
  {lt_1 : ∀ {x y : h.ι}, h.AncestralRel x y → h.dim x = h.dim y → rank_1 x < rank_1 y},
  { rank := rank, lt := lt } = { rank := rank_1, lt := lt_1 } → rank = rank_1

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank

Cited by

1 results in Mathlib

Foundations

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