II

📁 Source: Mathlib/AlgebraicTopology/SimplicialObject/II.lean

Statistics

Metric	Count
Definitions II, II, II, finset, map'	5
Theorems castSucc_mem_finset_iff, last_mem_finset, map'_eq_castSucc_iff, map'_eq_last_iff, map'_id, map'_last, map'_map', map'_predAbove, map'_succAboveOrderEmb, map'_zero, mem_finset_iff, monotone_map', nonempty_finset, II_obj, II_δ, II_σ	16
Total	21

SSet.Subcomplex.Pairing

Definitions

Name	Category	Theorems
II 📖	CompOp	15 math math: instFiniteSubtypeElemNIIAncestralRel, IsProper.isUniquelyCodimOneFace, dim_p, isUniquelyCodimOneFace, WeakRankFunction.wf_ancestralRel, RankFunction.wf_ancestralRel, IsRegular.wf, AncestralRel.dim_le, union, SSet.Subcomplex.PairingCore.pairing_II, instIsWellFoundedElemNIIAncestralRel, wf, exists_or, inter, SSet.Subcomplex.PairingCore.pairing_p_symm_equivI

SSet.Subcomplex.PairingCore

Definitions

Name	Category	Theorems
II 📖	CompOp	5 math math: pairing_p_equivII, ancestralRel_iff, equivII_apply_coe, pairing_II, pairing_p_symm_equivI

SimplexCategory

Definitions

Name	Category	Theorems
II 📖	CompOp	3 math math: II_σ, II_obj, II_δ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
II_obj 📖	mathematical	—	CategoryTheory.Functor.obj SimplexCategory smallCategory Opposite CategoryTheory.Category.opposite II Opposite.op len	—	—
II_δ 📖	mathematical	—	CategoryTheory.CosimplicialObject.δ Opposite SimplexCategory CategoryTheory.Category.opposite smallCategory II Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct σ	—	Hom.ext OrderHom.ext II.map'_succAboveOrderEmb
II_σ 📖	mathematical	—	CategoryTheory.CosimplicialObject.σ Opposite SimplexCategory CategoryTheory.Category.opposite smallCategory II Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct δ	—	Hom.ext OrderHom.ext II.map'_predAbove

SimplexCategory.II

Definitions

Name	Category	Theorems
finset 📖	CompOp	4 math math: castSucc_mem_finset_iff, last_mem_finset, nonempty_finset, mem_finset_iff
map' 📖	CompOp	9 math math: map'_last, map'_zero, map'_map', map'_eq_last_iff, map'_succAboveOrderEmb, map'_eq_castSucc_iff, monotone_map', map'_predAbove, map'_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
castSucc_mem_finset_iff 📖	mathematical	—	Finset Finset.instMembership finset DFunLike.coe OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike	—	—
last_mem_finset 📖	mathematical	—	Finset Finset.instMembership finset	—	instIsEmptyFalse
map'_eq_castSucc_iff 📖	mathematical	—	map' DFunLike.coe OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike	—	nonempty_finset LT.lt.not_ge Fin.eq_castSucc_or_eq_last
map'_eq_last_iff 📖	mathematical	—	map' DFunLike.coe OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike	—	nonempty_finset Fin.castSucc_ne_last Fin.eq_castSucc_of_ne_last LE.le.not_gt
map'_id 📖	mathematical	—	map' OrderHom.id PartialOrder.toPreorder Fin.instPartialOrder	—	Fin.eq_castSucc_or_eq_last map'_eq_castSucc_iff map'_last
map'_last 📖	mathematical	—	map'	—	—
map'_map' 📖	mathematical	—	map' OrderHom.comp PartialOrder.toPreorder Fin.instPartialOrder	—	Fin.eq_castSucc_or_eq_last map'_eq_castSucc_iff LE.le.trans OrderHom.monotone map'_eq_last_iff map'_last
map'_predAbove 📖	mathematical	—	map' PartialOrder.toPreorder Fin.instPartialOrder Fin.predAbove Fin.predAbove_right_monotone Fin.succAbove	—	Fin.predAbove_right_monotone Fin.eq_castSucc_or_eq_last Fin.succAbove_of_le_castSucc map'_eq_castSucc_iff Fin.ne_zero_of_lt LT.lt.le Fin.predAbove_of_castSucc_lt le_refl Fin.predAbove_of_le_castSucc Fin.castSucc_castPred lt_of_le_of_lt Fin.succAbove_of_castSucc_lt LT.lt.trans map'_last Fin.succAbove_ne_last_last
map'_succAboveOrderEmb 📖	mathematical	—	map' OrderEmbedding.toOrderHom PartialOrder.toPreorder Fin.instPartialOrder Fin.succAboveOrderEmb Fin.predAbove	—	Fin.eq_castSucc_or_eq_last Fin.predAbove_of_le_castSucc Iff.not LT.lt.ne Fin.castPred_castSucc LE.le.lt_or_eq Fin.succAbove_of_castSucc_lt le_refl Fin.succAbove_castSucc_self Fin.castSucc_le_succ lt_of_lt_of_le Fin.succAbove_last Fin.ne_zero_of_lt Fin.predAbove_of_castSucc_lt map'_eq_castSucc_iff Fin.succAbove_of_lt_succ LT.lt.le Fin.succAbove_of_le_castSucc map'_last Fin.predAbove_right_last
map'_zero 📖	mathematical	—	map'	—	—
mem_finset_iff 📖	mathematical	—	Finset Finset.instMembership finset DFunLike.coe OrderHom PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike Fin.castPred	—	—
monotone_map' 📖	mathematical	—	Monotone PartialOrder.toPreorder Fin.instPartialOrder map'	—	Finset.min'_subset nonempty_finset Fin.eq_castSucc_or_eq_last LE.le.trans
nonempty_finset 📖	mathematical	—	Finset.Nonempty finset	—	instIsEmptyFalse

---

← Back to Index