Documentation Verification Report

InitialSeg

📁 Source: Mathlib/Order/SuccPred/InitialSeg.lean

Statistics

Metric	Count
Definitions `InitialSeg`	1
Theorems `apply_covBy_apply_iff`, `apply_wCovBy_apply_iff`, `isSuccLimit_apply_iff`, `isSuccPrelimit_apply_iff`, `map_isSuccLimit`, `map_isSuccPrelimit`, `map_pred`, `map_succ`, `apply_covBy_apply_iff`, `apply_wCovBy_apply_iff`, `isSuccLimit_apply_iff`, `isSuccPrelimit_apply_iff`, `map_isSuccLimit`, `map_isSuccPrelimit`, `map_pred`, `map_succ`	16
Total	17

InitialSeg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_covBy_apply_iff` 📖	mathematical	—	`CovBy` `Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `InitialSeg` `instFunLike`	—	`Set.OrdConnected.apply_covBy_apply_iff` `IsLowerSet.ordConnected` `isLowerSet_range`
`apply_wCovBy_apply_iff` 📖	mathematical	—	`WCovBy` `PartialOrder.toPreorder` `DFunLike.coe` `InitialSeg` `Preorder.toLT` `instFunLike`	—	`instEmbeddingLike`
`isSuccLimit_apply_iff` 📖	mathematical	—	`Order.IsSuccLimit` `PartialOrder.toPreorder` `DFunLike.coe` `InitialSeg` `Preorder.toLT` `instFunLike`	—	—
`isSuccPrelimit_apply_iff` 📖	mathematical	—	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `InitialSeg` `instFunLike`	—	`apply_covBy_apply_iff` `mem_range_of_rel` `CovBy.lt`
`map_isSuccLimit` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder`	`DFunLike.coe` `InitialSeg` `Preorder.toLT` `instFunLike`	—	`isSuccLimit_apply_iff`
`map_isSuccPrelimit` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`DFunLike.coe` `InitialSeg` `instFunLike`	—	`isSuccPrelimit_apply_iff`
`map_pred` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `Preorder.toLT` `PartialOrder.toPreorder` `instFunLike` `Order.pred`	—	`CovBy.pred_eq` `apply_covBy_apply_iff` `Order.pred_covBy`
`map_succ` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `Preorder.toLT` `PartialOrder.toPreorder` `instFunLike` `Order.succ`	—	`CovBy.succ_eq` `apply_covBy_apply_iff` `Order.covBy_succ`

PrincipalSeg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_covBy_apply_iff` 📖	mathematical	—	`CovBy` `Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.apply_covBy_apply_iff` `mem_range_of_rel` `instIsTransLt`
`apply_wCovBy_apply_iff` 📖	mathematical	—	`WCovBy` `PartialOrder.toPreorder` `DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.apply_wCovBy_apply_iff` `mem_range_of_rel` `instIsTransLt`
`isSuccLimit_apply_iff` 📖	mathematical	—	`Order.IsSuccLimit` `PartialOrder.toPreorder` `DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.isSuccLimit_apply_iff` `mem_range_of_rel` `instIsTransLt`
`isSuccPrelimit_apply_iff` 📖	mathematical	—	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.isSuccPrelimit_apply_iff` `mem_range_of_rel` `instIsTransLt`
`map_isSuccLimit` 📖	mathematical	`Order.IsSuccLimit` `PartialOrder.toPreorder`	`DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`isSuccLimit_apply_iff`
`map_isSuccPrelimit` 📖	mathematical	`Order.IsSuccPrelimit` `Preorder.toLT` `PartialOrder.toPreorder`	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`isSuccPrelimit_apply_iff`
`map_pred` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `Preorder.toLT` `PartialOrder.toPreorder` `InitialSeg.instFunLike` `Order.pred`	—	`InitialSeg.map_pred`
`map_succ` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Preorder.toLT` `PartialOrder.toPreorder` `RelEmbedding.instFunLike` `toRelEmbedding` `Order.succ`	—	`InitialSeg.map_succ` `mem_range_of_rel` `instIsTransLt`

(root)

Definitions

Name	Category	Theorems
`InitialSeg` 📖	CompData	61 math math: `InitialSeg.trans_apply`, `InitialSeg.inj`, `PrincipalSeg.map_pred`, `InitialSeg.instRelHomClass`, `Ordinal.liftInitialSeg_coe`, `PrincipalSeg.transInitial_apply`, `InitialSeg.toOrderEmbedding_apply`, `InitialSeg.acc`, `InitialSeg.leAdd_apply`, `InitialSeg.monotone`, `InitialSeg.map_pred`, `InitialSeg.map_succ`, `CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot`, `InitialSeg.isNormal`, `InitialSeg.map_rel_iff`, `Ordinal.type_le_iff`, `Cardinal.liftInitialSeg_toFun`, `Set.initialSegIic_toFun`, `InitialSeg.exists_eq_iff_rel`, `InitialSeg.map_bot`, `InitialSeg.eq_relIso`, `CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit`, `InitialSeg.map_isMin`, `InitialSeg.image_Iio`, `InitialSeg.eq_principalSeg`, `InitialSeg.lt_apply_iff`, `InitialSeg.instSubsingletonOfIsWellOrder`, `InitialSeg.map_isSuccPrelimit`, `PrincipalSeg.coe_coe_fn'`, `OrderIso.toInitialSeg_toFun`, `PrincipalSeg.transInitial_top`, `CategoryTheory.TransfiniteCompositionOfShape.iic_F`, `CategoryTheory.SmallObject.restrictionLE_map`, `InitialSeg.lt_iff_lt`, `Ordinal.typein_apply`, `InitialSeg.instOrderHomClassLt`, `InitialSeg.transPrincipal_apply`, `InitialSeg.apply_wCovBy_apply_iff`, `InitialSeg.apply_covBy_apply_iff`, `InitialSeg.map_isSuccLimit`, `CategoryTheory.Functor.instIsWellOrderContinuousCompFunctor`, `Ordinal.lift_type_le`, `InitialSeg.subsingleton_of_trichotomous_of_irrefl`, `InitialSeg.strictMono`, `InitialSeg.antisymm_toFun`, `CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app`, `InitialSeg.isSuccLimit_apply_iff`, `InitialSeg.le_apply_iff`, `InitialSeg.eq_or_principal`, `InitialSeg.ext_iff`, `InitialSeg.instEmbeddingLike`, `RelIso.toInitialSeg_toFun`, `InitialSeg.isSuccPrelimit_apply_iff`, `InitialSeg.refl_apply`, `Set.initialSegIicIicOfLE_toFun_coe`, `InitialSeg.le_iff_le`, `InitialSeg.coe_toOrderEmbedding`, `InitialSeg.isLowerSet_range`, `InitialSeg.coe_coe_fn`, `InitialSeg.eq`, `InitialSeg.isMin_apply_iff`

---

← Back to Index