Theorems · Theorem · algebraic topology

SSet.Subcomplex.PairingCore.RankFunction.mk.injEq

∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} [inst : PartialOrder α] (rank : h.ι → α)
  (lt : ∀ {x y : h.ι}, h.AncestralRel x y → rank x < rank y) (rank_1 : h.ι → α)
  (lt_1 : ∀ {x y : h.ι}, h.AncestralRel x 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

0 results in Mathlib

Foundations

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

Assumes

PartialOrder