Documentation Verification Report

InitialSeg

📁 Source: Mathlib/Order/Interval/Set/InitialSeg.lean

Statistics

Metric	Count
Definitions `orderIsoIio`, `initialSegIic`, `initialSegIicIicOfLE`, `principalSegIio`, `principalSegIioIicOfLE`	5
Theorems `orderIsoIio_apply_coe`, `initialSegIicIicOfLE_toFun_coe`, `initialSegIic_toFun`, `principalSegIioIicOfLE_toRelEmbedding`, `principalSegIioIicOfLE_top`, `principalSegIio_toFun`, `principalSegIio_toRelEmbedding`, `principalSegIio_top`	8
Total	13

PrincipalSeg

Definitions

Name	Category	Theorems
`orderIsoIio` 📖	CompOp	1 math math: `orderIsoIio_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orderIsoIio_apply_coe` 📖	mathematical	—	`Set` `Set.instMembership` `Set.Iio` `PartialOrder.toPreorder` `top` `Preorder.toLT` `DFunLike.coe` `RelIso` `Set.Elem` `Preorder.toLE` `RelIso.instFunLike` `orderIsoIio` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	—

Set

Definitions

Name	Category	Theorems
`initialSegIic` 📖	CompOp	5 math math: `CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot`, `initialSegIic_toFun`, `CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit`, `CategoryTheory.TransfiniteCompositionOfShape.iic_F`, `CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app`
`initialSegIicIicOfLE` 📖	CompOp	2 math math: `CategoryTheory.SmallObject.restrictionLE_map`, `initialSegIicIicOfLE_toFun_coe`
`principalSegIio` 📖	CompOp	4 math math: `principalSegIio_toRelEmbedding`, `CategoryTheory.Functor.IsWellOrderContinuous.nonempty_isColimit`, `principalSegIio_toFun`, `principalSegIio_top`
`principalSegIioIicOfLE` 📖	CompOp	4 math math: `principalSegIioIicOfLE_toRelEmbedding`, `principalSegIioIicOfLE_top`, `CategoryTheory.SmallObject.restrictionLT_map`, `CategoryTheory.SmallObject.coconeOfLE_ι_app`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`initialSegIicIicOfLE_toFun_coe` 📖	mathematical	`Preorder.toLE`	`Set` `instMembership` `Iic` `DFunLike.coe` `InitialSeg` `Elem` `Preorder.toLT` `InitialSeg.instFunLike` `initialSegIicIicOfLE`	—	—
`initialSegIic_toFun` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `Elem` `Iic` `Preorder.toLT` `Set` `instMembership` `InitialSeg.instFunLike` `initialSegIic`	—	—
`principalSegIioIicOfLE_toRelEmbedding` 📖	mathematical	`Preorder.toLE`	`DFunLike.coe` `RelEmbedding` `Elem` `Iio` `Iic` `Preorder.toLT` `Set` `instMembership` `RelEmbedding.instFunLike` `PrincipalSeg.toRelEmbedding` `principalSegIioIicOfLE` `LE.le.trans` `LT.lt.le`	—	—
`principalSegIioIicOfLE_top` 📖	mathematical	`Preorder.toLE`	`PrincipalSeg.top` `Elem` `Iio` `Iic` `Preorder.toLT` `Set` `instMembership` `principalSegIioIicOfLE`	—	—
`principalSegIio_toFun` 📖	mathematical	—	`Function.Embedding.toFun` `Elem` `Iio` `RelEmbedding.toEmbedding` `Preorder.toLT` `Set` `instMembership` `PrincipalSeg.toRelEmbedding` `principalSegIio`	—	—
`principalSegIio_toRelEmbedding` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Elem` `Iio` `Preorder.toLT` `Set` `instMembership` `RelEmbedding.instFunLike` `PrincipalSeg.toRelEmbedding` `principalSegIio`	—	—
`principalSegIio_top` 📖	mathematical	—	`PrincipalSeg.top` `Elem` `Iio` `Preorder.toLT` `Set` `instMembership` `principalSegIio`	—	—

---

← Back to Index