Documentation Verification Report

Skeleton

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

Statistics

Metric	Count
Definitions `skeleton`, `skeletonOfMono`	2
Theorems `iSup_skeleton`, `iSup_skeletonOfMono`, `mem_skeleton`, `mem_skeletonOfMono_obj_iff_of_nonDegenerate`, `mem_skeleton_obj_iff_of_nonDegenerate`, `ofSimplex_le_skeleton`, `skeletonOfMono_obj_eq_top`, `skeletonOfMono_succ`, `skeletonOfMono_zero`, `skeleton_le_skeletonOfMono`, `skeleton_obj_eq_top`, `skeleton_succ`, `skeleton_zero`	13
Total	15

SSet

Definitions

Name	Category	Theorems
`skeleton` 📖	CompOp	8 math math: `ofSimplex_le_skeleton`, `iSup_skeleton`, `skeleton_le_skeletonOfMono`, `skeleton_obj_eq_top`, `mem_skeleton_obj_iff_of_nonDegenerate`, `skeleton_succ`, `mem_skeleton`, `skeleton_zero`
`skeletonOfMono` 📖	CompOp	6 math math: `skeleton_le_skeletonOfMono`, `skeletonOfMono_zero`, `iSup_skeletonOfMono`, `skeletonOfMono_obj_eq_top`, `mem_skeletonOfMono_obj_iff_of_nonDegenerate`, `skeletonOfMono_succ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup_skeleton` 📖	mathematical	—	`iSup` `Subcomplex` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `OrderHom.instFunLike` `skeleton` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`le_antisymm` `Subcomplex.le_iff_contains_nonDegenerate` `CategoryTheory.Subfunctor.iSup_obj` `mem_skeleton`
`iSup_skeletonOfMono` 📖	mathematical	—	`iSup` `Subcomplex` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `OrderHom.instFunLike` `skeletonOfMono` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`le_antisymm` `iSup_skeleton` `iSup_le_iff` `le_trans` `skeleton_le_skeletonOfMono` `le_iSup`
`mem_skeleton` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `DFunLike.coe` `OrderHom` `Subcomplex` `Nat.instPreorder` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `OrderHom.instFunLike` `skeleton`	—	`exists_nonDegenerate` `le_trans` `lt_of_le_of_lt` `SimplexCategory.len_le_of_epi` `le_refl` `le_iSup` `CategoryTheory.Subfunctor.map` `Subcomplex.mem_ofSimplex_obj`
`mem_skeletonOfMono_obj_iff_of_nonDegenerate` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `DFunLike.coe` `OrderHom` `Subcomplex` `Nat.instPreorder` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `OrderHom.instFunLike` `skeletonOfMono` `nonDegenerate` `Set.range` `CategoryTheory.NatTrans.app`	—	—
`mem_skeleton_obj_iff_of_nonDegenerate` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `CategoryTheory.types` `Opposite.op` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `DFunLike.coe` `OrderHom` `Subcomplex` `Nat.instPreorder` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `OrderHom.instFunLike` `skeleton` `nonDegenerate`	—	`CategoryTheory.Subfunctor.iSup_obj` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop` `mono_of_nonDegenerate` `SimplexCategory.len_le_of_mono` `mem_skeleton`
`ofSimplex_le_skeleton` 📖	mathematical	—	`Subcomplex` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `Subcomplex.ofSimplex` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike` `skeleton`	—	`mem_skeleton`
`skeletonOfMono_obj_eq_top` 📖	mathematical	—	`CategoryTheory.Subfunctor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `DFunLike.coe` `OrderHom` `Subcomplex` `Nat.instPreorder` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `OrderHom.instFunLike` `skeletonOfMono` `Opposite.op` `Top.top` `Set` `CategoryTheory.Functor.obj` `CategoryTheory.types` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra`	—	`top_le_iff` `skeleton_obj_eq_top` `le_sup_right`
`skeletonOfMono_succ` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Subcomplex` `Nat.instPreorder` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `OrderHom.instFunLike` `skeletonOfMono` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `iSup` `Set.Elem` `CategoryTheory.Functor.obj` `CategoryTheory.types` `Opposite.op` `nonDegenerate` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `Subcomplex.range` `Subcomplex.ofSimplex`	—	`le_antisymm` `skeleton_succ` `LE.le.trans` `le_sup_left` `le_sup_right` `le_trans` `le_refl` `le_iSup` `OrderHom.monotone` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `ofSimplex_le_skeleton` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `Nat.instZeroLEOneClass`
`skeletonOfMono_zero` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Subcomplex` `Nat.instPreorder` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `OrderHom.instFunLike` `skeletonOfMono` `Subcomplex.range`	—	`skeleton_zero` `sup_of_le_left`
`skeleton_le_skeletonOfMono` 📖	mathematical	—	`Subcomplex` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike` `skeleton` `skeletonOfMono`	—	`le_sup_right`
`skeleton_obj_eq_top` 📖	mathematical	—	`CategoryTheory.Subfunctor.obj` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `DFunLike.coe` `OrderHom` `Subcomplex` `Nat.instPreorder` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `OrderHom.instFunLike` `skeleton` `Opposite.op` `Top.top` `Set` `CategoryTheory.Functor.obj` `CategoryTheory.types` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra`	—	`top_le_iff` `mem_skeleton`
`skeleton_succ` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Subcomplex` `Nat.instPreorder` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `OrderHom.instFunLike` `skeleton` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `iSup` `Set.Elem` `CategoryTheory.Functor.obj` `CategoryTheory.types` `Opposite.op` `nonDegenerate` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Subcomplex.ofSimplex` `Set` `Set.instMembership`	—	`le_antisymm` `LE.le.lt_or_eq` `LE.le.trans` `ofSimplex_le_skeleton` `le_sup_left` `le_trans` `le_refl` `le_iSup` `le_sup_right` `OrderHom.monotone` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `Nat.instZeroLEOneClass`
`skeleton_zero` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Subcomplex` `Nat.instPreorder` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `Opposite` `SimplexCategory` `CategoryTheory.Category.opposite` `SimplexCategory.smallCategory` `OrderHom.instFunLike` `skeleton` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`Fin.isEmpty'`

---

← Back to Index