Rank

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Rank.lean

Statistics

Metric	Count
Definitions RankFunction, rank, toWeakRankFunction, WeakRankFunction, rank, RankFunction, rank, WeakRankFunction, rank, rankFunctionEquiv, weakRankFunctionEquiv	11
Theorems isRegular, lt, toWeakRankFunction_rank, wf_ancestralRel, isRegular, lt, wf_ancestralRel, lt, lt	9
Total	20

SSet.Subcomplex.Pairing

Definitions

Name	Category	Theorems
RankFunction 📖	CompData	2 math math: isRegular_iff_nonempty_rankFunction, instNonemptyRankFunctionNat
WeakRankFunction 📖	CompData	2 math math: instNonemptyWeakRankFunctionNat, isRegular_iff_nonempty_weakRankFunction

SSet.Subcomplex.Pairing.RankFunction

Definitions

Name	Category	Theorems
rank 📖	CompOp	2 math math: lt, toWeakRankFunction_rank
toWeakRankFunction 📖	CompOp	1 math math: toWeakRankFunction_rank

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRegular 📖	mathematical	—	SSet.Subcomplex.Pairing.IsRegular	—	wf_ancestralRel
lt 📖	mathematical	SSet.Subcomplex.Pairing.AncestralRel	Preorder.toLT PartialOrder.toPreorder rank	—	—
toWeakRankFunction_rank 📖	mathematical	—	SSet.Subcomplex.Pairing.WeakRankFunction.rank toWeakRankFunction rank	—	—
wf_ancestralRel 📖	mathematical	—	Set.Elem SSet.Subcomplex.N SSet.Subcomplex.Pairing.II SSet.Subcomplex.Pairing.AncestralRel	—	wellFounded_iff_isEmpty_descending_chain not_strictAnti_of_wellFoundedLT strictAnti_nat_of_succ_lt lt

SSet.Subcomplex.Pairing.WeakRankFunction

Definitions

Name	Category	Theorems
rank 📖	CompOp	2 math math: lt, SSet.Subcomplex.Pairing.RankFunction.toWeakRankFunction_rank

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isRegular 📖	mathematical	—	SSet.Subcomplex.Pairing.IsRegular	—	wf_ancestralRel
lt 📖	mathematical	SSet.Subcomplex.Pairing.AncestralRel SSet.S.dim SSet.N.toS SSet.Subcomplex.N.toN SSet.Subcomplex.N Set Set.instMembership SSet.Subcomplex.Pairing.II	Preorder.toLT PartialOrder.toPreorder rank	—	—
wf_ancestralRel 📖	mathematical	—	Set.Elem SSet.Subcomplex.N SSet.Subcomplex.Pairing.II SSet.Subcomplex.Pairing.AncestralRel	—	wellFounded_iff_isEmpty_descending_chain monotone_nat_of_le_succ SSet.Subcomplex.Pairing.AncestralRel.dim_le wellFoundedGT_iff_monotone_chain_condition IsWellOrder.toIsWellFounded isWellOrder_gt instWellFoundedGTOrderDualOfWellFoundedLT instWellFoundedLTNat not_strictAnti_of_wellFoundedLT strictAnti_nat_of_succ_lt add_assoc lt

SSet.Subcomplex.PairingCore

Definitions

Name	Category	Theorems
RankFunction 📖	CompData	—
WeakRankFunction 📖	CompData	—
rankFunctionEquiv 📖	CompOp	—
weakRankFunctionEquiv 📖	CompOp	—

SSet.Subcomplex.PairingCore.RankFunction

Definitions

Name	Category	Theorems
rank 📖	CompOp	1 math math: lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lt 📖	mathematical	SSet.Subcomplex.PairingCore.AncestralRel	Preorder.toLT PartialOrder.toPreorder rank	—	—

SSet.Subcomplex.PairingCore.WeakRankFunction

Definitions

Name	Category	Theorems
rank 📖	CompOp	1 math math: lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lt 📖	mathematical	SSet.Subcomplex.PairingCore.AncestralRel SSet.Subcomplex.PairingCore.dim	Preorder.toLT PartialOrder.toPreorder rank	—	—

---

← Back to Index