InitialSeg

📁 Source: Mathlib/Order/InitialSeg.lean

Statistics

Metric	Count
Definitions `antisymm`, `codRestrict`, `instCoeRelEmbedding`, `instFunLike`, `instInhabited`, `leAdd`, `ofIsEmpty`, `principalSumRelIso`, `refl`, `toOrderEmbedding`, `toPrincipalSeg`, `toRelEmbedding`, `total`, `trans`, `transPrincipal`, `«term_≺i_»`, `«term_≼i_»`, `toInitialSeg`, `codRestrict`, `hasCoeInitialSeg`, `instCoeFunForall`, `instCoeOutRelEmbedding`, `ofElement`, `ofIsEmpty`, `pemptyToPUnit`, `pemptyToPunit`, `relIsoTrans`, `subrelIso`, `toRelEmbedding`, `top`, `trans`, `transInitial`, `transRelIso`, `collapse`, `toInitialSeg`, `«term_, «term_≤i_»`	37
Theorems `acc`, `antisymm_symm`, `antisymm_toFun`, `codRestrict_apply`, `coe_coe_fn`, `coe_toOrderEmbedding`, `eq`, `eq_or_principal`, `eq_principalSeg`, `eq_relIso`, `exists_eq_iff_rel`, `exists_sum_relIso`, `ext`, `ext_iff`, `image_Iio`, `inj`, `instEmbeddingLike`, `instOrderHomClassLt`, `instRelHomClass`, `instSubsingletonOfIsWellOrder`, `isLowerSet_range`, `isMin_apply_iff`, `leAdd_apply`, `le_apply_iff`, `le_iff_le`, `lt_apply_iff`, `lt_iff_lt`, `map_bot`, `map_isMin`, `map_rel_iff`, `mem_range_of_le`, `mem_range_of_rel`, `mem_range_of_rel'`, `monotone`, `refl_apply`, `strictMono`, `subsingleton_of_trichotomous_of_irrefl`, `toOrderEmbedding_apply`, `toPrincipalSeg_apply`, `transPrincipal_apply`, `trans_apply`, `toInitialSeg_toFun`, `acc`, `apply_subrelIso`, `codRestrict_apply`, `codRestrict_top`, `coe_coe_fn'`, `coe_fn_mk`, `eq`, `exists_eq_iff_rel`, `ext`, `ext_iff`, `image_Iio`, `instIsEmptyOfIsWellOrder`, `instSubsingletonOfIsWellOrder`, `irrefl`, `isLowerSet_range`, `isMin_apply_iff`, `le_apply_iff`, `le_iff_le`, `lt_apply_iff`, `lt_iff_lt`, `lt_top`, `map_bot`, `map_isMin`, `mem_range_iff_rel`, `mem_range_iff_rel'`, `mem_range_of_le`, `mem_range_of_rel`, `mem_range_of_rel_top`, `monotone`, `ofElement_apply`, `ofElement_toFun`, `ofElement_top`, `ofIsEmpty_top`, `relIsoTrans_apply`, `relIsoTrans_top`, `strictMono`, `subrelIso_apply`, `subrelIso_symm_apply`, `surjOn`, `toRelEmbedding_inj`, `toRelEmbedding_injective`, `top_eq`, `top_rel_top`, `transInitial_apply`, `transInitial_top`, `transRelIso_apply`, `transRelIso_top`, `trans_apply`, `trans_top`, `toInitialSeg_toFun`, `wellFounded_iff_principalSeg`	93
Total	130

InitialSeg

Definitions

Name	Category	Theorems
`antisymm` 📖	CompOp	2 math math: `antisymm_symm`, `antisymm_toFun`
`codRestrict` 📖	CompOp	1 math math: `codRestrict_apply`
`instCoeRelEmbedding` 📖	CompOp	—
`instFunLike` 📖	CompOp	57 math math: `trans_apply`, `inj`, `PrincipalSeg.map_pred`, `instRelHomClass`, `Ordinal.liftInitialSeg_coe`, `PrincipalSeg.transInitial_apply`, `toOrderEmbedding_apply`, `acc`, `leAdd_apply`, `monotone`, `map_pred`, `map_succ`, `CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot`, `isNormal`, `map_rel_iff`, `Cardinal.liftInitialSeg_toFun`, `Set.initialSegIic_toFun`, `exists_eq_iff_rel`, `map_bot`, `eq_relIso`, `CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit`, `map_isMin`, `image_Iio`, `eq_principalSeg`, `lt_apply_iff`, `map_isSuccPrelimit`, `PrincipalSeg.coe_coe_fn'`, `OrderIso.toInitialSeg_toFun`, `PrincipalSeg.transInitial_top`, `CategoryTheory.TransfiniteCompositionOfShape.iic_F`, `CategoryTheory.SmallObject.restrictionLE_map`, `lt_iff_lt`, `Ordinal.typein_apply`, `instOrderHomClassLt`, `transPrincipal_apply`, `apply_wCovBy_apply_iff`, `apply_covBy_apply_iff`, `map_isSuccLimit`, `CategoryTheory.Functor.instIsWellOrderContinuousCompFunctor`, `strictMono`, `antisymm_toFun`, `CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app`, `isSuccLimit_apply_iff`, `le_apply_iff`, `eq_or_principal`, `ext_iff`, `instEmbeddingLike`, `RelIso.toInitialSeg_toFun`, `isSuccPrelimit_apply_iff`, `refl_apply`, `Set.initialSegIicIicOfLE_toFun_coe`, `le_iff_le`, `coe_toOrderEmbedding`, `isLowerSet_range`, `coe_coe_fn`, `eq`, `isMin_apply_iff`
`instInhabited` 📖	CompOp	—
`leAdd` 📖	CompOp	1 math math: `leAdd_apply`
`ofIsEmpty` 📖	CompOp	—
`principalSumRelIso` 📖	CompOp	—
`refl` 📖	CompOp	1 math math: `refl_apply`
`toOrderEmbedding` 📖	CompOp	2 math math: `toOrderEmbedding_apply`, `coe_toOrderEmbedding`
`toPrincipalSeg` 📖	CompOp	1 math math: `toPrincipalSeg_apply`
`toRelEmbedding` 📖	CompOp	1 math math: `coe_coe_fn`
`total` 📖	CompOp	—
`trans` 📖	CompOp	1 math math: `trans_apply`
`transPrincipal` 📖	CompOp	1 math math: `transPrincipal_apply`
`«term_≺i_»` 📖	CompOp	—
`«term_≼i_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acc` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `instFunLike`	—	`mem_range_of_rel` `map_rel_iff` `RelEmbedding.acc`
`antisymm_symm` 📖	mathematical	—	`RelIso.symm` `antisymm`	—	`RelIso.coe_fn_injective`
`antisymm_toFun` 📖	mathematical	—	`DFunLike.coe` `RelIso` `RelIso.instFunLike` `antisymm` `InitialSeg` `instFunLike`	—	—
`codRestrict_apply` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `InitialSeg` `instFunLike`	`Subrel` `codRestrict`	—	—
`coe_coe_fn` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `InitialSeg` `instFunLike`	—	—
`coe_toOrderEmbedding` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `instFunLikeOrderEmbedding` `toOrderEmbedding` `InitialSeg` `Preorder.toLT` `instFunLike`	—	—
`eq` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `instFunLike`	—	`instSubsingletonOfIsWellOrder`
`eq_or_principal` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `instFunLike` `Set` `Set.instMembership` `Set.range`	—	`IsWellFounded.induction` `IsWellOrder.toIsWellFounded` `Mathlib.Tactic.Push.not_forall_eq` `trichotomous` `IsWellOrder.toTrichotomous` `mem_range_of_rel` `Set.mem_range_self`
`eq_principalSeg` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `PrincipalSeg.toRelEmbedding` `InitialSeg` `instFunLike`	—	`eq` `PrincipalSeg.mem_range_of_rel` `IsWellOrder.toIsTrans`
`eq_relIso` 📖	mathematical	—	`DFunLike.coe` `RelIso` `RelIso.instFunLike` `InitialSeg` `instFunLike`	—	`eq`
`exists_eq_iff_rel` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `instFunLike`	—	`mem_range_of_rel` `map_rel_iff`
`exists_sum_relIso` 📖	mathematical	—	`IsWellOrder` `RelIso`	—	`Subrel.instIsWellOrderSubtype` `IsWellOrder.toIsTrans` `IsWellOrder.toTrichotomous` `instIsWellOrderOfIsEmpty` `PEmpty.instIsEmpty`
`ext` 📖	—	`DFunLike.coe` `InitialSeg` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `instFunLike`	—	`ext`
`image_Iio` 📖	mathematical	—	`Set.image` `DFunLike.coe` `InitialSeg` `Preorder.toLT` `PartialOrder.toPreorder` `instFunLike` `Set.Iio`	—	`OrderEmbedding.image_Iio` `isLowerSet_range`
`inj` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `instFunLike`	—	—
`instEmbeddingLike` 📖	mathematical	—	`EmbeddingLike` `InitialSeg` `instFunLike`	—	`Function.Embedding.inj'`
`instOrderHomClassLt` 📖	mathematical	—	`OrderHomClass` `InitialSeg` `Preorder.toLT` `PartialOrder.toPreorder` `Preorder.toLE` `instFunLike`	—	`RelEmbedding.map_rel_iff`
`instRelHomClass` 📖	mathematical	—	`RelHomClass` `InitialSeg` `instFunLike`	—	`RelEmbedding.map_rel_iff`
`instSubsingletonOfIsWellOrder` 📖	mathematical	—	`InitialSeg`	—	`RelEmbedding.isWellFounded` `IsWellOrder.toIsWellFounded` `subsingleton_of_trichotomous_of_irrefl` `IsWellOrder.toTrichotomous` `IsStrictOrder.toIrrefl` `IsStrictTotalOrder.toIsStrictOrder` `instIsStrictTotalOrderOfIsWellOrder`
`isLowerSet_range` 📖	mathematical	—	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `Set.range` `DFunLike.coe` `InitialSeg` `Preorder.toLT` `instFunLike`	—	`mem_range_of_le`
`isMin_apply_iff` 📖	mathematical	—	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `InitialSeg` `Preorder.toLT` `instFunLike`	—	`StrictMono.isMin_of_apply` `strictMono` `mem_range_of_le` `le_iff_le`
`leAdd_apply` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `instFunLike` `leAdd`	—	—
`le_apply_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `InitialSeg` `Preorder.toLT` `instFunLike`	—	`mem_range_of_le` `le_iff_le` `monotone`
`le_iff_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `InitialSeg` `Preorder.toLT` `instFunLike`	—	`OrderEmbedding.le_iff_le`
`lt_apply_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `InitialSeg` `instFunLike`	—	`mem_range_of_rel` `lt_iff_lt` `strictMono`
`lt_iff_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `InitialSeg` `instFunLike`	—	`OrderEmbedding.lt_iff_lt`
`map_bot` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `Preorder.toLT` `PartialOrder.toPreorder` `instFunLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`IsMin.eq_bot` `map_isMin` `isMin_bot`
`map_isMin` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder`	`DFunLike.coe` `InitialSeg` `Preorder.toLT` `instFunLike`	—	`isMin_apply_iff`
`map_rel_iff` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `instFunLike`	—	`RelEmbedding.map_rel_iff'`
`mem_range_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `InitialSeg` `Preorder.toLT` `instFunLike`	`Set` `Set.instMembership` `Set.range`	—	`LE.le.eq_or_lt` `mem_range_of_rel`
`mem_range_of_rel` 📖	mathematical	`DFunLike.coe` `InitialSeg` `instFunLike`	`Set` `Set.instMembership` `Set.range`	—	`mem_range_of_rel'`
`mem_range_of_rel'` 📖	mathematical	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	`Set` `Set.instMembership` `Set.range`	—	—
`monotone` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `DFunLike.coe` `InitialSeg` `Preorder.toLT` `instFunLike`	—	`OrderEmbedding.monotone`
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `instFunLike` `refl`	—	—
`strictMono` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `DFunLike.coe` `InitialSeg` `Preorder.toLT` `instFunLike`	—	`OrderEmbedding.strictMono`
`subsingleton_of_trichotomous_of_irrefl` 📖	mathematical	—	`InitialSeg`	—	`ext` `IsWellFounded.induction` `extensional_of_trichotomous_of_irrefl` `exists_eq_iff_rel`
`toOrderEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `PartialOrder.toPreorder` `instFunLikeOrderEmbedding` `toOrderEmbedding` `InitialSeg` `Preorder.toLT` `instFunLike`	—	—
`toPrincipalSeg_apply` 📖	mathematical	`DFunLike.coe` `InitialSeg` `instFunLike`	`RelEmbedding` `RelEmbedding.instFunLike` `PrincipalSeg.toRelEmbedding` `toPrincipalSeg`	—	—
`transPrincipal_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `PrincipalSeg.toRelEmbedding` `transPrincipal` `InitialSeg` `instFunLike`	—	`transPrincipal.eq_1` `PrincipalSeg.trans_apply` `eq_principalSeg` `PrincipalSeg.relIsoTrans_apply` `eq_relIso`
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `instFunLike` `trans`	—	—

OrderIso

Definitions

Name	Category	Theorems
`toInitialSeg` 📖	CompOp	1 math math: `toInitialSeg_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toInitialSeg_toFun` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `Preorder.toLT` `InitialSeg.instFunLike` `toInitialSeg` `OrderIso` `Preorder.toLE` `instFunLikeOrderIso`	—	—

PrincipalSeg

Definitions

Name	Category	Theorems
`codRestrict` 📖	CompOp	2 math math: `codRestrict_apply`, `codRestrict_top`
`hasCoeInitialSeg` 📖	CompOp	—
`instCoeFunForall` 📖	CompOp	—
`instCoeOutRelEmbedding` 📖	CompOp	—
`ofElement` 📖	CompOp	3 math math: `ofElement_top`, `ofElement_apply`, `ofElement_toFun`
`ofIsEmpty` 📖	CompOp	1 math math: `ofIsEmpty_top`
`pemptyToPUnit` 📖	CompOp	—
`pemptyToPunit` 📖	CompOp	—
`relIsoTrans` 📖	CompOp	2 math math: `relIsoTrans_apply`, `relIsoTrans_top`
`subrelIso` 📖	CompOp	3 math math: `apply_subrelIso`, `subrelIso_symm_apply`, `subrelIso_apply`
`toRelEmbedding` 📖	CompOp	87 math math: `trans_apply`, `Ordinal.typein_le_typein`, `Ordinal.mem_range_typein_iff`, `map_succ`, `Ordinal.iSup_typein_succ`, `isLowerSet_range`, `isMin_apply_iff`, `InitialSeg.toPrincipalSeg_apply`, `Set.principalSegIioIicOfLE_toRelEmbedding`, `mem_range_iff_rel`, `transInitial_apply`, `Ordinal.enum_symm_apply_coe`, `mem_range_iff_rel'`, `isSuccLimit_apply_iff`, `exists_eq_iff_rel`, `map_bot`, `le_iff_le`, `mem_range_of_rel_top`, `Ordinal.typein_top`, `Ordinal.bfamilyOfFamily'_typein`, `isSuccPrelimit_apply_iff`, `Ordinal.liftPrincipalSeg_coe`, `apply_covBy_apply_iff`, `monotone`, `Ordinal.typein_lt_type`, `apply_wCovBy_apply_iff`, `Ordinal.typein_lt_typein`, `lt_top`, `apply_subrelIso`, `cocone_ι_app`, `Set.principalSegIio_toRelEmbedding`, `transRelIso_apply`, `IsWellFounded.rank_eq_typein`, `strictMono`, `InitialSeg.eq_principalSeg`, `CategoryTheory.Functor.IsWellOrderContinuous.nonempty_isColimit`, `Ordinal.type_subrel`, `ext_iff`, `Ordinal.enum_typein`, `trans_top`, `Cardinal.card_typein_lt`, `Cardinal.card_typein_toType_lt`, `Ordinal.blsub_type`, `coe_coe_fn'`, `relIsoTrans_apply`, `cocone_pt`, `orderIsoIio_apply_coe`, `lt_apply_iff`, `ofElement_apply`, `Ordinal.bfamilyOfFamily_typein`, `Ordinal.typein_enum`, `subrelIso_symm_apply`, `map_isSuccPrelimit`, `Ordinal.typein_surj`, `Ordinal.typein_injective`, `Ordinal.typein_apply`, `Ordinal.ToType.mk_symm_apply_coe`, `InitialSeg.transPrincipal_apply`, `toRelEmbedding_injective`, `Ordinal.typein_surjOn`, `Ordinal.iSup_typein_limit`, `isNormal`, `Ordinal.card_typein`, `Ordinal.lift_typein_top`, `Ordinal.typein_ordinal`, `Ordinal.lsub_typein`, `surjOn`, `acc`, `Ordinal.typein_lt_self`, `map_isSuccLimit`, `eq`, `Ordinal.typein_one_toType`, `toRelEmbedding_inj`, `Ordinal.sup_typein_limit`, `CategoryTheory.SmallObject.restrictionLT_map`, `Ordinal.typein_le_typein'`, `Set.principalSegIio_toFun`, `CategoryTheory.SmallObject.coconeOfLE_ι_app`, `Ordinal.typein_inj`, `subrelIso_apply`, `le_apply_iff`, `coe_fn_mk`, `map_isMin`, `image_Iio`, `Ordinal.sup_typein_succ`, `lt_iff_lt`, `ofElement_toFun`
`top` 📖	CompOp	28 math math: `mem_range_iff_rel`, `Ordinal.liftPrincipalSeg_top'`, `Ordinal.enum_symm_apply_coe`, `transRelIso_top`, `mem_range_iff_rel'`, `top_eq`, `Ordinal.typein_top`, `Set.principalSegIioIicOfLE_top`, `lt_top`, `ofIsEmpty_top`, `apply_subrelIso`, `cocone_ι_app`, `ofElement_top`, `trans_top`, `transInitial_top`, `top_rel_top`, `cocone_pt`, `orderIsoIio_apply_coe`, `subrelIso_symm_apply`, `Ordinal.lift_typein_top`, `surjOn`, `relIsoTrans_top`, `CategoryTheory.SmallObject.coconeOfLE_ι_app`, `subrelIso_apply`, `Ordinal.top_typein`, `Ordinal.liftPrincipalSeg_top`, `Ordinal.enum_type`, `Set.principalSegIio_top`
`trans` 📖	CompOp	2 math math: `trans_apply`, `trans_top`
`transInitial` 📖	CompOp	2 math math: `transInitial_apply`, `transInitial_top`
`transRelIso` 📖	CompOp	2 math math: `transRelIso_top`, `transRelIso_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acc` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.acc` `mem_range_of_rel`
`apply_subrelIso` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `RelIso` `top` `Subrel` `RelIso.instFunLike` `subrelIso`	—	`Equiv.apply_ofInjective_symm` `RelEmbedding.injective`
`codRestrict_apply` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `top`	`Subrel` `codRestrict`	—	—
`codRestrict_top` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `top`	`Subrel` `codRestrict`	—	—
`coe_coe_fn'` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `InitialSeg.instFunLike` `toRelEmbedding` `mem_range_of_rel` `RelEmbedding` `RelEmbedding.instFunLike`	—	`mem_range_of_rel`
`coe_fn_mk` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike`	`toRelEmbedding`	—	—
`eq` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`instSubsingletonOfIsWellOrder`
`exists_eq_iff_rel` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.exists_eq_iff_rel` `mem_range_of_rel`
`ext` 📖	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	—	`RelEmbedding.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`ext`
`image_Iio` 📖	mathematical	—	`Set.image` `DFunLike.coe` `RelEmbedding` `Preorder.toLT` `PartialOrder.toPreorder` `RelEmbedding.instFunLike` `toRelEmbedding` `Set.Iio`	—	`InitialSeg.image_Iio` `mem_range_of_rel` `instIsTransLt`
`instIsEmptyOfIsWellOrder` 📖	mathematical	—	`IsEmpty` `PrincipalSeg`	—	`irrefl`
`instSubsingletonOfIsWellOrder` 📖	mathematical	—	`PrincipalSeg`	—	`ext` `IsStrictOrder.toIrrefl` `IsStrictTotalOrder.toIsStrictOrder` `instIsStrictTotalOrderOfIsWellOrder` `IsWellOrder.toTrichotomous` `InitialSeg.eq` `mem_range_of_rel` `IsWellOrder.toIsTrans`
`irrefl` 📖	—	—	—	—	`lt_top` `irrefl` `IsStrictOrder.toIrrefl` `IsStrictTotalOrder.toIsStrictOrder` `instIsStrictTotalOrderOfIsWellOrder` `InitialSeg.eq` `mem_range_of_rel` `IsWellOrder.toIsTrans`
`isLowerSet_range` 📖	mathematical	—	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `Set.range` `DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.isLowerSet_range` `mem_range_of_rel` `instIsTransLt`
`isMin_apply_iff` 📖	mathematical	—	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.isMin_apply_iff` `mem_range_of_rel` `instIsTransLt`
`le_apply_iff` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.le_apply_iff` `mem_range_of_rel` `instIsTransLt`
`le_iff_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.le_iff_le` `mem_range_of_rel` `instIsTransLt`
`lt_apply_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.lt_apply_iff` `mem_range_of_rel` `instIsTransLt`
`lt_iff_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.lt_iff_lt` `mem_range_of_rel` `instIsTransLt`
`lt_top` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `top`	—	`mem_range_iff_rel`
`map_bot` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Preorder.toLT` `PartialOrder.toPreorder` `RelEmbedding.instFunLike` `toRelEmbedding` `Bot.bot` `OrderBot.toBot` `Preorder.toLE`	—	`InitialSeg.map_bot` `mem_range_of_rel` `instIsTransLt`
`map_isMin` 📖	mathematical	`IsMin` `Preorder.toLE` `PartialOrder.toPreorder`	`DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`isMin_apply_iff`
`mem_range_iff_rel` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `top`	—	`mem_range_iff_rel'`
`mem_range_iff_rel'` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `top`	—	—
`mem_range_of_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `toRelEmbedding`	`Set` `Set.instMembership` `Set.range`	—	`InitialSeg.mem_range_of_le` `mem_range_of_rel` `instIsTransLt`
`mem_range_of_rel` 📖	mathematical	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	`Set` `Set.instMembership` `Set.range`	—	`mem_range_of_rel_top` `trans` `lt_top`
`mem_range_of_rel_top` 📖	mathematical	`top`	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`mem_range_iff_rel`
`monotone` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.monotone` `mem_range_of_rel` `instIsTransLt`
`ofElement_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Subrel` `RelEmbedding.instFunLike` `toRelEmbedding` `ofElement`	—	—
`ofElement_toFun` 📖	mathematical	—	`Function.Embedding.toFun` `RelEmbedding.toEmbedding` `Subrel` `toRelEmbedding` `ofElement`	—	—
`ofElement_top` 📖	mathematical	—	`top` `Subrel` `ofElement`	—	—
`ofIsEmpty_top` 📖	mathematical	—	`top` `ofIsEmpty`	—	—
`relIsoTrans_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `relIsoTrans` `RelIso` `RelIso.instFunLike`	—	—
`relIsoTrans_top` 📖	mathematical	—	`top` `relIsoTrans`	—	—
`strictMono` 📖	mathematical	—	`StrictMono` `PartialOrder.toPreorder` `DFunLike.coe` `RelEmbedding` `Preorder.toLT` `RelEmbedding.instFunLike` `toRelEmbedding`	—	`InitialSeg.strictMono` `mem_range_of_rel` `instIsTransLt`
`subrelIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `top` `Subrel` `RelIso.instFunLike` `subrelIso` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `lt_top`	—	`Equiv.ofInjective_symm_apply` `RelEmbedding.injective`
`subrelIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `top` `Subrel` `RelIso.instFunLike` `RelIso.symm` `subrelIso` `Equiv` `Set.Elem` `Set.range` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.setCongr` `Set` `Set.instMembership`	—	—
`surjOn` 📖	mathematical	—	`Set.SurjOn` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `Set.univ` `setOf` `top`	—	`Set.image_univ` `mem_range_of_rel_top`
`toRelEmbedding_inj` 📖	mathematical	—	`toRelEmbedding`	—	`toRelEmbedding_injective`
`toRelEmbedding_injective` 📖	mathematical	—	`PrincipalSeg` `RelEmbedding` `toRelEmbedding`	—	`extensional_of_trichotomous_of_irrefl`
`top_eq` 📖	mathematical	—	`top`	—	`instSubsingletonOfIsWellOrder`
`top_rel_top` 📖	mathematical	—	`top`	—	`IsWellOrder.toIsTrans` `instSubsingletonOfIsWellOrder` `lt_top`
`transInitial_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `transInitial` `InitialSeg` `InitialSeg.instFunLike`	—	—
`transInitial_top` 📖	mathematical	—	`top` `transInitial` `DFunLike.coe` `InitialSeg` `InitialSeg.instFunLike`	—	—
`transRelIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `transRelIso` `RelIso` `RelIso.instFunLike`	—	—
`transRelIso_top` 📖	mathematical	—	`top` `transRelIso` `DFunLike.coe` `RelIso` `RelIso.instFunLike`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `trans`	—	—
`trans_top` 📖	mathematical	—	`top` `trans` `DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding`	—	—

RelEmbedding

Definitions

Name	Category	Theorems
`collapse` 📖	CompOp	—

RelIso

Definitions

Name	Category	Theorems
`toInitialSeg` 📖	CompOp	1 math math: `toInitialSeg_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toInitialSeg_toFun` 📖	mathematical	—	`DFunLike.coe` `InitialSeg` `InitialSeg.instFunLike` `toInitialSeg` `RelIso` `instFunLike`	—	—

(root)

Definitions

Name	Category	Theorems
`«term_` `📖`	CompOp	—
`«term_≤i_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellFounded_iff_principalSeg` 📖	—	—	—	—	`RelHomClass.wellFounded` `RelEmbedding.instRelHomClass` `wellFounded_iff_wellFounded_subrel`

---

← Back to Index