NerveNondegenerate

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/NerveNondegenerate.lean

Statistics

Metric	Count
Definitions	0
Theorems mem_nerve_degenerate_of_eq, mem_nerve_nonDegenerate_iff_injective, mem_nerve_nonDegenerate_iff_strictMono, mem_range_nerve_σ_iff	4
Total	4

PartialOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_nerve_degenerate_of_eq 📖	mathematical	CategoryTheory.Functor.obj SimplexCategory.len Opposite.unop SimplexCategory Opposite.op Preorder.smallCategory toPreorder Fin.instPartialOrder	Opposite CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.nerve Set Set.instMembership SSet.degenerate	—	SSet.degenerate_eq_iUnion_range_σ mem_range_nerve_σ_iff
mem_nerve_nonDegenerate_iff_injective 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.nerve Preorder.smallCategory toPreorder Opposite.op Set Set.instMembership SSet.nonDegenerate SimplexCategory.len Opposite.unop Fin.instPartialOrder	—	mem_nerve_nonDegenerate_iff_strictMono StrictMono.injective LE.le.lt_or_eq CategoryTheory.Functor.monotone LT.lt.le Eq.not_lt
mem_nerve_nonDegenerate_iff_strictMono 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.nerve Preorder.smallCategory toPreorder Opposite.op Set Set.instMembership SSet.nonDegenerate StrictMono SimplexCategory.len Opposite.unop Fin.instPartialOrder	—	SSet.nondegenerate_zero Subsingleton.strictMono not_iff_not SSet.mem_degenerate_iff_notMem_nonDegenerate Fin.strictMono_iff_lt_succ SSet.degenerate_eq_iUnion_range_σ Set.mem_iUnion CategoryTheory.Functor.monotone Fin.castSucc_le_succ
mem_range_nerve_σ_iff 📖	mathematical	—	CategoryTheory.Functor.obj Opposite SimplexCategory CategoryTheory.Category.opposite SimplexCategory.smallCategory CategoryTheory.types CategoryTheory.nerve Preorder.smallCategory toPreorder Opposite.op Set Set.instMembership Set.range CategoryTheory.SimplicialObject.σ SimplexCategory.len Opposite.unop Fin.instPartialOrder	—	Fin.predAbove_castSucc_self Fin.predAbove_succ_self CategoryTheory.nerve.ext_of_isThin Preorder.subsingleton_hom CategoryTheory.nerve.σ_obj CategoryTheory.nerve.δ_obj Fin.ne_zero_of_lt Fin.predAbove_of_castSucc_lt Fin.succAbove_of_le_castSucc

---

← Back to Index