Basic

📁 Source: Mathlib/Order/RelIso/Basic.lean

Statistics

Metric	Count
Definitions `mkRelHom`, `outRelEmbedding`, `RelEmbedding`, `instCoeRelHom`, `instFunLike`, `instInhabited`, `ofIsEmpty`, `ofMapRelIff`, `ofMonotone`, `preimage`, `prodLexMap`, `prodLexMkLeft`, `prodLexMkRight`, `refl`, `sumLexInl`, `sumLexInr`, `sumLexMap`, `sumLiftRelInl`, `sumLiftRelInr`, `sumLiftRelMap`, `swap`, `toEmbedding`, `toRelHom`, `trans`, `RelHom`, `comp`, `id`, `instFunLike`, `preimage`, `swap`, `toFun`, `RelHomClass`, `RelIso`, `apply`, `symm_apply`, `cast`, `compl`, `copy`, `emptySumLex`, `instCoeOutRelEmbedding`, `instEquivLike`, `instFunLike`, `instInhabited`, `ofSurjective`, `ofUniqueOfIrrefl`, `ofUniqueOfRefl`, `preimage`, `prodLexCongr`, `refl`, `relHomCongr`, `relIsoOfIsEmpty`, `sumLexCongr`, `sumLexEmpty`, `swap`, `toEquiv`, `toRelEmbedding`, `trans`, `relEmbedding`, `«term_→r_»`, `«term_↪r_»`, `«term_≃r_»`	61
Theorems `wellFounded_iff`, `mkRelHom_apply`, `outRelEmbedding_apply`, `acc`, `antisymm`, `asymm`, `coe_fn_injective`, `coe_mk`, `coe_toEmbedding`, `coe_toRelHom`, `coe_trans`, `eq_preimage`, `ext`, `ext_iff`, `inj`, `injective`, `instEmbeddingLike`, `instRelHomClass`, `irrefl`, `isAntisymm`, `isAsymm`, `isIrrefl`, `isLinearOrder`, `isPartialOrder`, `isPreorder`, `isRefl`, `isStrictOrder`, `isStrictTotalOrder`, `isSymm`, `isTotal`, `isTrans`, `isTrichotomous`, `isWellFounded`, `isWellOrder`, `map_rel_iff`, `map_rel_iff'`, `ofMapRelIff_coe`, `ofMonotone_coe`, `preimage_apply`, `prodLexMap_apply`, `prodLexMkLeft_apply`, `prodLexMkRight_apply`, `refl_apply`, `stdRefl`, `sumLexInl_apply`, `sumLexInr_apply`, `sumLexMap_apply`, `sumLiftRelInl_apply`, `sumLiftRelInr_apply`, `sumLiftRelMap_apply`, `swap_apply`, `toEmbedding_inj`, `toEmbedding_injective`, `total`, `trans_apply`, `trichotomous`, `wellFounded`, `coeFn_mk`, `coe_fn_injective`, `coe_fn_toFun`, `comp_apply`, `ext`, `ext_iff`, `id_apply`, `injective_of_increasing`, `instRelHomClass`, `map_rel`, `map_rel'`, `preimage_apply`, `swap_apply`, `acc`, `asymm`, `irrefl`, `isAsymm`, `isIrrefl`, `isWellFounded`, `map_rel`, `wellFounded`, `preimage`, `ulift`, `apply_eq_iff_eq`, `apply_eq_iff_eq_symm_apply`, `apply_symm_apply`, `bijective`, `cast_apply`, `cast_refl`, `cast_symm`, `cast_toEquiv`, `cast_trans`, `coe_copy`, `coe_fn_injective`, `coe_fn_mk`, `coe_fn_symm_mk`, `coe_fn_toEquiv`, `coe_toEmbedding`, `coe_toRelEmbedding`, `compl_apply`, `compl_symm_apply`, `copy_eq`, `default_def`, `emptySumLex_apply`, `emptySumLex_symm_apply`, `eq_iff_eq`, `eq_symm_apply`, `ext`, `ext_iff`, `injective`, `instRelHomClass`, `map_rel_iff`, `map_rel_iff'`, `ofSurjective_apply`, `preimage_apply`, `preimage_symm_apply`, `refl_apply`, `refl_symm`, `refl_trans`, `relHomCongr_apply`, `relHomCongr_symm_apply`, `rel_symm_apply`, `self_comp_symm`, `self_trans_symm`, `sumLexEmpty_apply`, `sumLexEmpty_symm_apply`, `surjective`, `symm_apply_apply`, `symm_apply_eq`, `symm_apply_rel`, `symm_bijective`, `symm_comp_self`, `symm_symm`, `symm_symm_apply`, `symm_trans_apply`, `symm_trans_self`, `toEquiv_injective`, `trans_apply`, `trans_assoc`, `trans_refl`, `relEmbedding_apply`, `wellFoundedGT`, `wellFoundedLT`, `of_quotient_liftOn₂'`, `of_quotient_lift₂`, `quotient_liftOn₂'`, `quotient_lift₂`, `acc_liftOn₂'_iff`, `acc_lift₂_iff`, `injective_of_increasing`, `preimage_equivalence`, `wellFounded_liftOn₂'_iff`, `wellFounded_lift₂_iff`	150
Total	211

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wellFounded_iff` 📖	—	—	—	—	`RelHomClass.wellFounded` `RelHom.instRelHomClass` `Function.surjInv_eq`

Quotient

Definitions

Name	Category	Theorems
`mkRelHom` 📖	CompOp	1 math math: `mkRelHom_apply`
`outRelEmbedding` 📖	CompOp	1 math math: `outRelEmbedding_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mkRelHom_apply` 📖	mathematical	—	`DFunLike.coe` `RelHom` `RelHom.instFunLike` `mkRelHom`	—	—
`outRelEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `outRelEmbedding` `out`	—	—

RelEmbedding

Definitions

Name	Category	Theorems
`instCoeRelHom` 📖	CompOp	—
`instFunLike` 📖	CompOp	203 math math: `AddUnits.orderEmbeddingVal_apply`, `Set.chainHeight_eq_of_relEmbedding`, `PrincipalSeg.trans_apply`, `Fin.valOrderEmb_apply`, `Ordinal.typein_le_typein`, `Ordinal.mem_range_typein_iff`, `PrincipalSeg.map_succ`, `OrderEmbedding.mulRight_apply`, `Ordinal.iSup_typein_succ`, `PrincipalSeg.isLowerSet_range`, `PrincipalSeg.isMin_apply_iff`, `InitialSeg.toPrincipalSeg_apply`, `Set.principalSegIioIicOfLE_toRelEmbedding`, `coe_one`, `PrincipalSeg.mem_range_iff_rel`, `SimpleGraph.Path.mapEmbedding_coe`, `PrincipalSeg.transInitial_apply`, `Ordinal.enum_symm_apply_coe`, `PrincipalSeg.mem_range_iff_rel'`, `smul_def`, `PrincipalSeg.isSuccLimit_apply_iff`, `SimpleGraph.Embedding.apply_mem_neighborSet_iff`, `SimpleGraph.Embedding.sumInr_apply`, `SimpleGraph.EdgeLabeling.get_pullback`, `sumLiftRelInr_apply`, `PrincipalSeg.exists_eq_iff_rel`, `SimpleGraph.Copy.topEmbedding_apply`, `PrincipalSeg.map_bot`, `IsAntichain.image_relEmbedding`, `AddLocalization.mkOrderEmbedding_apply`, `PrincipalSeg.le_iff_le`, `PrincipalSeg.mem_range_of_rel_top`, `IsChain.image_relEmbedding`, `preimage_apply`, `LieSubmodule.toSubmodule_orderEmbedding_apply`, `SimpleGraph.Embedding.map_adj_iff`, `sumLexMap_apply`, `Ordinal.typein_top`, `SimpleGraph.completeMultipartiteGraph.topEmbedding_apply_fst`, `Localization.mkOrderEmbedding_apply`, `NonemptyInterval.toDualProdHom_apply`, `Ordinal.bfamilyOfFamily'_typein`, `sumLexInl_apply`, `injective`, `IsChain.image_relEmbedding_iff`, `SimpleGraph.Embedding.sumInl_apply`, `SimpleGraph.Embedding.mapNeighborSet_apply_coe`, `PrincipalSeg.isSuccPrelimit_apply_iff`, `coe_toEmbedding`, `Ordinal.liftPrincipalSeg_coe`, `PrincipalSeg.apply_covBy_apply_iff`, `Fin.natAddOrderEmb_apply`, `SimpleGraph.Embedding.map_mem_edgeSet_iff`, `Units.orderEmbeddingVal_apply`, `OrderEmbedding.withTopCoe_apply`, `one_apply`, `instRelHomClass`, `Quotient.outRelEmbedding_apply`, `PrincipalSeg.monotone`, `Ordinal.typein_lt_type`, `Nat.castOrderEmbedding_apply`, `PrincipalSeg.apply_wCovBy_apply_iff`, `Ordinal.typein_lt_typein`, `HahnSeries.embDomainOrderEmbedding_apply`, `PrincipalSeg.lt_top`, `instEmbeddingLike`, `PrincipalSeg.apply_subrelIso`, `ofMonotone_coe`, `PrincipalSeg.cocone_ι_app`, `Set.principalSegIio_toRelEmbedding`, `PrincipalSeg.transRelIso_apply`, `IsWellFounded.rank_eq_typein`, `SSet.stdSimplex.nonDegenerateEquiv_apply_apply`, `coe_fn_injective`, `coe_toRelHom`, `PrincipalSeg.strictMono`, `InitialSeg.eq_principalSeg`, `CategoryTheory.Functor.IsWellOrderContinuous.nonempty_isColimit`, `pairwise_swap_listMap`, `ENat.toENNRealOrderEmbedding_apply`, `prodLexMkRight_apply`, `orderEmbeddingOfInjective_apply`, `Ordinal.type_subrel`, `pairwise_listMap`, `PrincipalSeg.ext_iff`, `sumLexInr_apply`, `Set.wellFoundedOn_iff_no_descending_seq`, `Ordinal.enum_typein`, `sumLiftRelMap_apply`, `Subrel.relEmbedding_apply`, `PrincipalSeg.trans_top`, `Cardinal.card_typein_lt`, `Cardinal.card_typein_toType_lt`, `OrderEmbedding.withTopMap_apply`, `Ordinal.blsub_type`, `PrincipalSeg.coe_coe_fn'`, `SimpleGraph.Embedding.coe_comp`, `PrincipalSeg.relIsoTrans_apply`, `coe_trans`, `map_rel_iff`, `PrincipalSeg.cocone_pt`, `Finsupp.orderEmbeddingToFun_apply`, `PrincipalSeg.orderIsoIio_apply_coe`, `PrincipalSeg.lt_apply_iff`, `PrincipalSeg.ofElement_apply`, `SSet.orderEmbeddingN_apply`, `Ordinal.bfamilyOfFamily_typein`, `Ordinal.typein_enum`, `SimpleGraph.induceHomOfLE_apply`, `PrincipalSeg.subrelIso_symm_apply`, `PrincipalSeg.map_isSuccPrelimit`, `Ordinal.typein_surj`, `Ordinal.typein_injective`, `inj`, `eq_preimage`, `refl_apply`, `Rat.castOrderEmbedding_apply`, `Ordinal.typein_apply`, `Ordinal.ToType.mk_symm_apply_coe`, `InitialSeg.transPrincipal_apply`, `Field.Emb.Cardinal.filtration_apply`, `SimpleGraph.Path.mapEmbedding_injective`, `PrimeSpectrum.nhdsOrderEmbedding_apply`, `Ordinal.typein_surjOn`, `OrderEmbedding.withBotCoe_apply`, `sumLiftRelInl_apply`, `OrderEmbedding.addRight_apply`, `Ordinal.iSup_typein_limit`, `ofMapRelIff_coe`, `PrincipalSeg.isNormal`, `Ordinal.card_typein`, `Ordinal.lift_typein_top`, `prodLexMap_apply`, `Ordinal.typein_ordinal`, `coe_natLT`, `acc_iff_isEmpty_subtype_mem_range`, `OrderEmbedding.gtEmbedding_apply`, `WithTop.coeOrderHom_apply`, `coe_natGT`, `Ordinal.lsub_typein`, `OrderEmbedding.orderIso_apply`, `Multiset.mapEmbedding_apply`, `ext_iff`, `PrincipalSeg.surjOn`, `OrderEmbedding.addLeft_apply`, `PrincipalSeg.acc`, `SimpleGraph.Embedding.map_apply`, `Fin.castSuccOrderEmb_apply`, `Ordinal.typein_lt_self`, `SimpleGraph.completeMultipartiteGraph.topEmbedding_apply_snd`, `PrincipalSeg.map_isSuccLimit`, `orderEmbeddingOfLTEmbedding_apply`, `SimpleGraph.Embedding.comap_apply`, `PrincipalSeg.eq`, `LieSubmodule.mapOrderEmbedding_apply`, `TwoSidedIdeal.coeOrderEmbedding_apply`, `not_acc`, `WithBot.coeOrderHom_apply`, `Ordinal.typein_one_toType`, `sorted_listMap`, `SimpleGraph.Embedding.coe_completeGraph`, `CompleteLatticeHom.toOrderIsoRangeOfInjective_apply`, `Ordinal.sup_typein_limit`, `mul_apply`, `CategoryTheory.SmallObject.restrictionLT_map`, `Ordinal.typein_le_typein'`, `SimpleGraph.Embedding.coe_toHom`, `OrderEmbedding.ltEmbedding_apply`, `coe_mul`, `Subtype.orderEmbedding_apply_coe`, `SimpleGraph.boxProdRight_apply`, `CategoryTheory.SmallObject.coconeOfLE_ι_app`, `sorted_swap_listMap`, `IsChain.preimage_relEmbedding`, `prodLexMkLeft_apply`, `Submodule.restrictScalarsEmbedding_apply`, `OrderEmbedding.ofAntisymmetrization_apply`, `IsAntichain.preimage_relEmbedding`, `Ordinal.typein_inj`, `PrincipalSeg.subrelIso_apply`, `RelIso.coe_toRelEmbedding`, `Subtype.relEmbedding_apply`, `OrderEmbedding.withBotMap_apply`, `coe_mk`, `IsAntichain.image_relEmbedding_iff`, `PrincipalSeg.le_apply_iff`, `Fin.castLEOrderEmb_apply`, `Subrel.coe_inclusionEmbedding`, `InitialSeg.coe_coe_fn`, `Fin.castAddOrderEmb_apply`, `OrderEmbedding.ofIsEmpty_apply`, `SimpleGraph.boxProdLeft_apply`, `Ordinal.toPGameEmbedding_apply`, `NNRat.castOrderEmbedding_apply`, `trans_apply`, `OrderEmbedding.mulLeft_apply`, `PrincipalSeg.map_isMin`, `PrincipalSeg.image_Iio`, `Ordinal.sup_typein_succ`, `Fin.addNatOrderEmb_apply`, `Fin.succAboveOrderEmb_apply`, `PrincipalSeg.lt_iff_lt`, `swap_apply`
`instInhabited` 📖	CompOp	—
`ofIsEmpty` 📖	CompOp	—
`ofMapRelIff` 📖	CompOp	1 math math: `ofMapRelIff_coe`
`ofMonotone` 📖	CompOp	1 math math: `ofMonotone_coe`
`preimage` 📖	CompOp	1 math math: `preimage_apply`
`prodLexMap` 📖	CompOp	1 math math: `prodLexMap_apply`
`prodLexMkLeft` 📖	CompOp	1 math math: `prodLexMkLeft_apply`
`prodLexMkRight` 📖	CompOp	1 math math: `prodLexMkRight_apply`
`refl` 📖	CompOp	4 math math: `PartOrdEmb.hom_id`, `PartOrdEmb.ofHom_id`, `refl_apply`, `one_def`
`sumLexInl` 📖	CompOp	1 math math: `sumLexInl_apply`
`sumLexInr` 📖	CompOp	1 math math: `sumLexInr_apply`
`sumLexMap` 📖	CompOp	1 math math: `sumLexMap_apply`
`sumLiftRelInl` 📖	CompOp	1 math math: `sumLiftRelInl_apply`
`sumLiftRelInr` 📖	CompOp	1 math math: `sumLiftRelInr_apply`
`sumLiftRelMap` 📖	CompOp	1 math math: `sumLiftRelMap_apply`
`swap` 📖	CompOp	1 math math: `swap_apply`
`toEmbedding` 📖	CompOp	17 math math: `Fin.addNatOrderEmb_toEmbedding`, `Fin.castSuccOrderEmb_toEmbedding`, `Fin.natAddOrderEmb_toEmbedding`, `coe_toEmbedding`, `toEmbedding_inj`, `Equiv.finsetCongr_toEmbedding`, `Finset.powersetCard_map`, `Fin.castLEOrderEmb_toEmbedding`, `Fin.castAddOrderEmb_toEmbedding`, `Fin.succAboveOrderEmb_toEmbedding`, `Finset.map_orderEmbOfFin_univ`, `toEmbedding_injective`, `Set.principalSegIio_toFun`, `Fin.succOrderEmb_toEmbedding`, `map_rel_iff'`, `Set.powersetCard.ofFinEmbEquiv_apply`, `PrincipalSeg.ofElement_toFun`
`toRelHom` 📖	CompOp	12 math math: `RelIso.relHomCongr_symm_apply`, `SimpleGraph.Iso.connectedComponentEquiv_symm_apply`, `SimpleGraph.EdgeLabeling.get_pullback`, `RelIso.relHomCongr_apply`, `coe_toRelHom`, `SimpleGraph.ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map`, `SimpleGraph.ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp`, `SimpleGraph.Embedding.mapEdgeSet_apply`, `SimpleGraph.Iso.mapEdgeSet_apply`, `SimpleGraph.Iso.connectedComponentEquiv_apply`, `SimpleGraph.Iso.mapEdgeSet_symm_apply`, `toOrderHom_injective`
`trans` 📖	CompOp	6 math math: `PartOrdEmb.hom_comp`, `mul_def`, `coe_trans`, `PartOrdEmb.ofHom_comp`, `Finset.orderEmbOfFin_compl_singleton`, `trans_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acc` 📖	—	`DFunLike.coe` `RelEmbedding` `instFunLike`	—	—	`map_rel_iff`
`antisymm` 📖	—	—	—	—	`Function.Embedding.inj'`
`asymm` 📖	—	—	—	—	`asymm` `map_rel_iff`
`coe_fn_injective` 📖	mathematical	—	`RelEmbedding` `DFunLike.coe` `instFunLike`	—	`DFunLike.coe_injective`
`coe_mk` 📖	mathematical	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	`RelEmbedding` `instFunLike`	—	—
`coe_toEmbedding` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `toEmbedding` `RelEmbedding` `instFunLike`	—	—
`coe_toRelHom` 📖	mathematical	—	`DFunLike.coe` `RelHom` `RelHom.instFunLike` `toRelHom` `RelEmbedding` `instFunLike`	—	—
`coe_trans` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `trans`	—	—
`eq_preimage` 📖	mathematical	—	`Order.Preimage` `DFunLike.coe` `RelEmbedding` `instFunLike`	—	`map_rel_iff`
`ext` 📖	—	`DFunLike.coe` `RelEmbedding` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike`	—	`ext`
`inj` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike`	—	`injective`
`injective` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike`	—	`Function.Embedding.inj'`
`instEmbeddingLike` 📖	mathematical	—	`EmbeddingLike` `RelEmbedding` `instFunLike`	—	`Function.Embedding.inj'`
`instRelHomClass` 📖	mathematical	—	`RelHomClass` `RelEmbedding` `instFunLike`	—	`map_rel_iff'`
`irrefl` 📖	—	—	—	—	`map_rel_iff` `irrefl`
`isAntisymm` 📖	—	—	—	—	`antisymm`
`isAsymm` 📖	—	—	—	—	`asymm`
`isIrrefl` 📖	—	—	—	—	`irrefl`
`isLinearOrder` 📖	mathematical	—	`IsLinearOrder`	—	`isPartialOrder` `IsLinearOrder.toIsPartialOrder` `total` `IsLinearOrder.toTotal`
`isPartialOrder` 📖	mathematical	—	`IsPartialOrder`	—	`isPreorder` `IsPartialOrder.toIsPreorder` `antisymm` `IsPartialOrder.toAntisymm`
`isPreorder` 📖	mathematical	—	`IsPreorder`	—	`stdRefl` `IsPreorder.toRefl` `isTrans` `IsPreorder.toIsTrans`
`isRefl` 📖	—	—	—	—	`stdRefl`
`isStrictOrder` 📖	mathematical	—	`IsStrictOrder`	—	`irrefl` `IsStrictOrder.toIrrefl` `isTrans` `IsStrictOrder.toIsTrans`
`isStrictTotalOrder` 📖	mathematical	—	`IsStrictTotalOrder`	—	`trichotomous` `IsStrictTotalOrder.toTrichotomous` `isStrictOrder` `IsStrictTotalOrder.toIsStrictOrder`
`isSymm` 📖	—	—	—	—	`symm`
`isTotal` 📖	—	—	—	—	`total`
`isTrans` 📖	mathematical	—	`IsTrans`	—	—
`isTrichotomous` 📖	—	—	—	—	`trichotomous`
`isWellFounded` 📖	mathematical	—	`IsWellFounded`	—	`wellFounded` `IsWellFounded.wf`
`isWellOrder` 📖	mathematical	—	`IsWellOrder`	—	`isStrictTotalOrder` `instIsStrictTotalOrderOfIsWellOrder` `IsStrictTotalOrder.toTrichotomous` `IsStrictOrder.toIsTrans` `IsStrictTotalOrder.toIsStrictOrder` `wellFounded` `IsWellFounded.wf` `IsWellOrder.toIsWellFounded`
`map_rel_iff` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike`	—	`map_rel_iff'`
`map_rel_iff'` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `toEmbedding`	—	—
`ofMapRelIff_coe` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `ofMapRelIff`	—	—
`ofMonotone_coe` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `ofMonotone`	—	—
`preimage_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Order.Preimage` `Function.Embedding` `Function.instFunLikeEmbedding` `instFunLike` `preimage`	—	—
`prodLexMap_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `prodLexMap`	—	—
`prodLexMkLeft_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `prodLexMkLeft`	—	—
`prodLexMkRight_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `prodLexMkRight`	—	—
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `refl`	—	—
`stdRefl` 📖	—	—	—	—	`map_rel_iff` `refl`
`sumLexInl_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `sumLexInl`	—	—
`sumLexInr_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `sumLexInr`	—	—
`sumLexMap_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `sumLexMap`	—	—
`sumLiftRelInl_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `sumLiftRelInl`	—	—
`sumLiftRelInr_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `sumLiftRelInr`	—	—
`sumLiftRelMap_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `sumLiftRelMap`	—	—
`swap_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Function.swap` `instFunLike` `swap`	—	—
`toEmbedding_inj` 📖	mathematical	—	`toEmbedding`	—	`toEmbedding_injective`
`toEmbedding_injective` 📖	mathematical	—	`RelEmbedding` `Function.Embedding` `toEmbedding`	—	—
`total` 📖	—	—	—	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `instFunLike` `trans`	—	—
`trichotomous` 📖	—	—	—	—	`Function.Embedding.injective` `Iff.not`
`wellFounded` 📖	—	—	—	—	`acc`

RelHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	4 math math: `RelIso.relHomCongr_symm_apply`, `RelIso.relHomCongr_apply`, `mul_def`, `comp_apply`
`id` 📖	CompOp	2 math math: `one_def`, `id_apply`
`instFunLike` 📖	CompOp	85 math math: `SimpleGraph.map_singletonSubgraph`, `SimpleGraph.Walk.map_copy`, `SimpleGraph.homOfConnectedComponents_apply`, `SimpleGraph.Coloring.mem_colorClass`, `swap_apply`, `SimpleGraph.Subgraph.spanningHom_injective`, `SimpleGraph.card_le_chromaticNumber_iff_forall_surjective`, `one_apply`, `coeFn_mk`, `SimpleGraph.Subgraph.comap_verts`, `SimpleGraph.Copy.toHom_apply`, `SimpleGraph.Hom.coe_id`, `mul_apply`, `SimpleGraph.Copy.injective`, `SimpleGraph.Walk.darts_map`, `SimpleGraph.Walk.map_nil`, `SimpleGraph.Hom.map_adj`, `SimpleGraph.Walk.map_map`, `SimpleGraph.Hom.mapEdgeSet_coe`, `instRelHomClass`, `SimpleGraph.Hom.map_mem_edgeSet`, `RelEmbedding.coe_toRelHom`, `coe_fn_injective`, `coe_fn_toFun`, `toOrderHom_coe`, `SimpleGraph.Hom.mapDart_apply`, `SimpleGraph.Walk.IsSubwalk.map`, `SimpleGraph.Subgraph.edgeSet_map`, `SimpleGraph.le_chromaticNumber_iff_forall_surjective`, `SimpleGraph.Subgraph.map_verts`, `SimpleGraph.ConnectedComponent.toSimpleGraph_hom_apply`, `SimpleGraph.Hom.comap_apply`, `SimpleGraph.Coloring.injective_comp_of_pairwise_adj`, `coe_one`, `SimpleGraph.Copy.injective'`, `SimpleGraph.Hom.coe_comp`, `SimpleGraph.Subgraph.map_adj`, `SimpleGraph.Walk.reverse_map`, `SimpleGraph.colorable_iff_exists_bdd_nat_coloring`, `Quotient.mkRelHom_apply`, `SimpleGraph.Walk.length_map`, `SimpleGraph.Subgraph.hom_injective`, `preimage_apply`, `SimpleGraph.Reachable.map`, `SimpleGraph.Hom.mapNeighborSet_coe`, `SimpleGraph.ConnectedComponent.map_mk`, `smul_def`, `SimpleGraph.Subgraph.spanningHom_apply`, `SimpleGraph.Walk.map_cons`, `RelSeries.last_map`, `SimpleGraph.Walk.edgeSet_map`, `SimpleGraph.Coloring.surjOn_of_card_le_isClique`, `comp_apply`, `RelSeries.head_map`, `SimpleGraph.Walk.map_append`, `RelSeries.map_apply`, `SimpleGraph.Walk.map_eq_of_eq`, `SimpleGraph.Embedding.coe_toHom`, `map_rel`, `SimpleGraph.Coloring.odd_length_iff_not_congr`, `SimpleGraph.Subgraph.inclusion_apply_coe`, `SimpleGraph.Walk.support_map`, `SimpleGraph.chromaticNumber_eq_iff_forall_surjective`, `SimpleGraph.Walk.edges_map`, `SimpleGraph.Reachable.coe_subgraphMap`, `SimpleGraph.Subgraph.hom_apply`, `SimpleGraph.Coloring.mem_colorClasses`, `SimpleGraph.Hom.injective_of_top_hom`, `injective_of_increasing`, `SimpleGraph.map_subgraphOfAdj`, `SimpleGraph.Hom.coe_ofLE`, `id_apply`, `ext_iff`, `SimpleGraph.Walk.map_eq_nil_iff`, `coe_mul`, `SimpleGraph.Subgraph.inclusion.injective`, `SimpleGraph.Coloring.even_length_iff_congr`, `SimpleGraph.Walk.getVert_map`, `SimpleGraph.chromaticNumber_eq_card_iff_forall_surjective`, `SimpleGraph.Walk.toSubgraph_map`, `SimpleGraph.Subgraph.coe_hom`, `SimpleGraph.Subgraph.comap_adj`, `SimpleGraph.Hom.apply_mem_neighborSet`, `SimpleGraph.Copy.coe_toHom`, `SimpleGraph.Hom.ofLE_apply`
`preimage` 📖	CompOp	1 math math: `preimage_apply`
`swap` 📖	CompOp	1 math math: `swap_apply`
`toFun` 📖	CompOp	2 math math: `coe_fn_toFun`, `map_rel'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeFn_mk` 📖	mathematical	—	`DFunLike.coe` `RelHom` `instFunLike`	—	—
`coe_fn_injective` 📖	mathematical	—	`RelHom` `DFunLike.coe` `instFunLike`	—	`DFunLike.coe_injective`
`coe_fn_toFun` 📖	mathematical	—	`toFun` `DFunLike.coe` `RelHom` `instFunLike`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `RelHom` `instFunLike` `comp`	—	—
`ext` 📖	—	`DFunLike.coe` `RelHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `RelHom` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `RelHom` `instFunLike` `id`	—	—
`injective_of_increasing` 📖	mathematical	—	`DFunLike.coe` `RelHom` `instFunLike`	—	`injective_of_increasing` `map_rel`
`instRelHomClass` 📖	mathematical	—	`RelHomClass` `RelHom` `instFunLike`	—	`map_rel'`
`map_rel` 📖	mathematical	—	`DFunLike.coe` `RelHom` `instFunLike`	—	`map_rel'`
`map_rel'` 📖	mathematical	—	`toFun`	—	—
`preimage_apply` 📖	mathematical	—	`DFunLike.coe` `RelHom` `Order.Preimage` `instFunLike` `preimage`	—	—
`swap_apply` 📖	mathematical	—	`DFunLike.coe` `RelHom` `Function.swap` `instFunLike` `swap`	—	—

RelHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acc` 📖	—	`DFunLike.coe`	—	—	`map_rel`
`asymm` 📖	—	—	—	—	`map_rel`
`irrefl` 📖	—	—	—	—	`map_rel`
`isAsymm` 📖	—	—	—	—	`asymm`
`isIrrefl` 📖	—	—	—	—	`irrefl`
`isWellFounded` 📖	mathematical	—	`IsWellFounded`	—	`wellFounded` `IsWellFounded.wf`
`map_rel` 📖	mathematical	—	`DFunLike.coe`	—	—
`wellFounded` 📖	—	—	—	—	`acc`

RelIso

Definitions

Name	Category	Theorems
`cast` 📖	CompOp	5 math math: `cast_refl`, `cast_apply`, `cast_symm`, `cast_trans`, `cast_toEquiv`
`compl` 📖	CompOp	2 math math: `compl_apply`, `compl_symm_apply`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`emptySumLex` 📖	CompOp	2 math math: `emptySumLex_apply`, `emptySumLex_symm_apply`
`instCoeOutRelEmbedding` 📖	CompOp	—
`instEquivLike` 📖	CompOp	2 math math: `compl_apply`, `compl_symm_apply`
`instFunLike` 📖	CompOp	373 math math: `IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal`, `WithZero.logOrderIso_apply`, `SimpleGraph.Iso.map_adj_iff`, `TwoSidedIdeal.orderIsoRingCon_symm_apply`, `WithZero.val_expOrderIso_apply`, `ULift.orderIso_symm_apply_down`, `YoungDiagram.transposeOrderIso_symm_apply`, `one_apply`, `SimpleGraph.isVertexCover_preimage_iso`, `OrderIso.arrowCongr_apply`, `OrderIso.sumCongr_apply`, `Subgroup.MapSubtype.orderIso_apply_coe`, `OrderIso.withTopCongr_apply`, `Submonoid.coe_invOrderIso_apply`, `IsLocalization.AtPrime.coe_orderIsoOfPrime_apply_coe`, `RingEquiv.idealComapOrderIso_apply`, `Ordinal.isInitialIso_apply`, `sumLexComplRight_apply`, `smul_def`, `OrderIso.mulRight₀_symm_apply`, `OrderIso.smulRight_apply`, `TopologicalSpace.Closeds.complOrderIso_symm_apply`, `PrimeSpectrum.equivSubtype_apply_coe`, `AddSubsemigroup.coe_toSubsemigroup_symm_apply`, `upperSetIsoLowerSet_apply`, `OrderIso.toRelIsoLT_apply`, `PrimeSpectrum.equivSubtype_symm_apply_asIdeal`, `IsMaxChain.image`, `TwoSidedIdeal.orderIsoRingCon_apply`, `OrderIso.divRight_symm_apply`, `OrderIso.neg_apply`, `ENNReal.mulRightOrderIso_symm_apply`, `coe_fn_symm_mk`, `OrderHom.piIso_symm_apply`, `IsAntichain.image_relIso_iff`, `Ordinal.enum_symm_apply_coe`, `PrincipalSeg.transRelIso_top`, `MulEquiv.comapSubgroup_symm_apply`, `Ordinal.enum_zero_le`, `Submonoid.coe_invOrderIso_symm_apply`, `sumLexComplLeft_symm_apply`, `IsChain.image_relIso`, `Ordinal.enum_lt_enum`, `NNReal.orderIsoRpow_apply`, `Ordinal.isInitialIso_symm_apply_coe`, `SimpleGraph.Iso.reachable_iff`, `OrderIso.subLeft_apply`, `Subsemigroup.opEquiv_symm_apply`, `preimage_eq_image_symm`, `IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal`, `mul_apply`, `TopologicalSpace.Opens.complOrderIso_apply`, `eq_iff_eq`, `Homeomorph.opensCongr_apply`, `OrderIso.inv_symm_apply`, `OrderIso.addRight_apply`, `AddSubmonoid.coe_toSubmonoid_apply`, `SimpleGraph.Iso.sumComm_apply`, `OrderHom.prodIso_apply`, `AddSubsemigroup.coe_toSubsemigroup_apply`, `StrictMono.orderIso_apply`, `TwoSidedIdeal.orderIsoMatrix_apply_ringCon_r`, `IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe`, `OrderIso.prodAssoc_apply`, `SimpleGraph.Iso.sumBoxProdDistrib_apply`, `SimpleGraph.Iso.symm_apply_reachable`, `TopologicalSpace.Opens.complOrderIso_symm_apply`, `SimpleGraph.hasseDualIso_apply`, `MulEquiv.mapSubgroup_apply`, `OrderIso.mulRight₀_apply`, `Equiv.toOrderIsoSet_symm_apply`, `cast_apply`, `LieSubmodule.orderIsoMapComap_apply`, `SimpleGraph.induceUnivIso_apply`, `SimpleGraph.Iso.map_symm_apply`, `OrderIso.smulRightDual_apply`, `Fin.revOrderIso_apply`, `Prod.Lex.prodLexAssoc_symm_apply`, `OrderIso.setIsotypicComponents_apply`, `WithZero.expOrderIso_symm_apply`, `IsLocalization.AtPrime.coe_primeSpectrumOrderIso_apply_coe_asIdeal`, `Ordinal.enum_le_enum'`, `PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal`, `Fin.insertNthOrderIso_symm_apply`, `InitialSeg.eq_relIso`, `OrderIso.ofRelIsoLT_apply`, `emptySumLex_apply`, `OrderIso.divRight₀_symm_apply`, `OrderIso.mulLeft₀_apply`, `IsGalois.intermediateFieldEquivSubgroup_apply`, `bijective`, `CategoryTheory.Abelian.subobjectIsoSubobjectOp_apply`, `OrderIso.finsetSetFinite_symm_apply`, `coe_toEmbedding`, `TwoSidedIdeal.orderIsoIsTwoSided_symm_apply`, `TwoSidedIdeal.opOrderIso_symm_apply`, `OrderIso.divLeft_apply`, `OrderIso.coe_toRelIsoLT`, `coe_one`, `Prod.Lex.sumLexProdLexDistrib_symm_apply`, `Sum.Lex.toLexRelIsoLE_coe`, `coe_mul`, `OrderIso.subRight_symm_apply`, `ext_iff`, `IsChain.image_relIso_iff`, `OrderIso.withBotCongr_symm_apply`, `Subsemiring.opEquiv_apply`, `upperSetIsoLowerSet_symm_apply`, `ENNReal.orderIsoIicOneBirational_apply_coe`, `IntermediateField.extendScalars.orderIso_apply`, `symm_apply_eq`, `OrderIso.withZeroUnits_symm_apply`, `TopologicalSpace.Closeds.complOrderIso_apply`, `OrderIso.ofHomInv_apply`, `LieSubmodule.orderIsoMapComap_symm_apply`, `SimpleGraph.Iso.map_mem_edgeSet_iff`, `AddSubsemigroup.opEquiv_symm_apply`, `infIccOrderIsoIccSup_apply_coe`, `sumLexEmpty_symm_apply`, `ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier`, `PrincipalSeg.apply_subrelIso`, `subrelUnivIso_symm_apply`, `coe_fn_injective`, `StrictMono.orderIsoOfRightInverse_symm_apply`, `SimpleGraph.boxProdComm_symm_apply`, `OrderIso.setCongr_symm_apply`, `OrderIso.smulRight_symm_apply`, `PrincipalSeg.transRelIso_apply`, `compl_apply`, `infIooOrderIsoIooSup_symm_apply_coe`, `CategoryTheory.Subobject.mapIsoToOrderIso_apply`, `SimpleGraph.Iso.apply_mem_neighborSet_iff`, `AddSubmonoid.coe_negOrderIso_symm_apply`, `Con.orderIsoOp_symm_apply`, `Subrepresentation.submoduleSubrepresentationOrderIso_apply`, `instRelHomClass`, `symm_apply_apply`, `SimpleGraph.boxProdAssoc_apply`, `ENNReal.mulRightOrderIso_apply`, `rel_symm_apply`, `AddEquiv.mapAddSubgroup_symm_apply`, `Subgroup.coe_toAddSubgroup_symm_apply`, `Fin.castOrderIso_apply`, `Sum.Lex.toLexRelIsoLE_symm_coe`, `Prod.Lex.sumLexProdLexDistrib_apply`, `OrderIso.arrowCongr_symm_apply`, `IsAntichain.image_relIso`, `Sublattice.prodEquiv_apply`, `RingCon.opOrderIso_apply`, `mkFactorOrderIsoOfFactorDvdEquiv_apply_coe`, `WithZero.val_inv_expOrderIso_apply`, `OrderIso.compl_symm_apply`, `OrderIso.prodAssoc_symm_apply`, `TwoSidedIdeal.opOrderIso_apply`, `SimpleGraph.ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map`, `IsChain.preimage_relIso`, `apply_eq_iff_eq`, `inv_apply_self`, `OrderIso.sumLexCongr_apply`, `Concept.swapEquiv_apply`, `Subgroup.orderIsoCon_apply`, `OrderIso.ofUnique_symm_apply`, `apply_eq_iff_eq_symm_apply`, `Ordinal.le_enum_succ`, `ENNReal.mulLeftOrderIso_symm_apply`, `Fin.snocOrderIso_apply`, `symm_apply_rel`, `AddEquiv.comapAddSubgroup_apply`, `Ordinal.enum_typein`, `injective`, `Set.chainHeight_eq_of_relIso`, `symm_comp_self`, `OrderIso.divRight₀_apply`, `SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning_apply_coe`, `AddSubgroup.orderIsoAddCon_symm_apply_coe`, `MulEquiv.mapSubgroup_symm_apply`, `symm_symm_apply`, `PrincipalSeg.relIsoTrans_apply`, `CategoryTheory.Subfunctor.orderIsoSubobject_apply`, `ofSurjective_apply`, `Fin.orderIsoSubtype_apply`, `SimpleGraph.isVertexCover_image_iso`, `Submodule.orderIsoMapComapOfBijective_symm_apply`, `Fin.snocOrderIso_symm_apply`, `OrderIso.divRight_apply`, `Subsemiring.opEquiv_symm_apply`, `PrincipalSeg.orderIsoIio_apply_coe`, `Fin.consOrderIso_apply`, `ULift.orderIso_apply`, `Ordinal.typein_enum`, `AddSubgroup.opEquiv_symm_apply`, `OrderIso.ofUnique_apply`, `PrincipalSeg.subrelIso_symm_apply`, `Real.sinhOrderIso_apply`, `OrderIso.subRight_apply`, `AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe`, `sumLexComplRight_symm_apply`, `Ordinal.toZFSetIso_apply`, `pairwise_swap_listMap`, `PrimeSpectrum.comapEquiv_apply`, `SimpleGraph.ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp`, `MulEquiv.comapSubgroup_apply`, `AddSubgroup.MapSubtype.orderIso_apply_coe`, `OrderIso.withBotCongr_apply`, `Ordinal.ToType.mk_symm_apply_coe`, `SimpleGraph.Iso.mapNeighborSet_apply_coe`, `Subgroup.coe_toAddSubgroup_apply`, `Submodule.orderIsoMapComap_apply`, `SimpleGraph.Iso.comap_apply`, `refl_apply`, `apply_symm_apply`, `Ordinal.enum_succ_eq_top`, `OrderIso.coe_symm_toRelIsoGT`, `compl_symm_apply`, `OrderIso.sumComm_apply`, `symm_trans_apply`, `OrderIso.neg_symm_apply`, `RingCon.opOrderIso_symm_apply`, `Fin.castLEOrderIso_symm_apply`, `Fin.consOrderIso_symm_apply`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal`, `OrderIso.invENNReal_apply`, `Subsemigroup.opEquiv_apply`, `SimpleGraph.Iso.boxProdSumDistrib_symm_apply`, `infIooOrderIsoIooSup_apply_coe`, `IntermediateField.extendScalars.orderIso_symm_apply_coe`, `AddEquiv.mapAddSubgroup_apply`, `OrderIso.mulLeft₀_symm_apply`, `Sum.Lex.toLexRelIsoLT_coe`, `Ordinal.enum_le_enum`, `OrderIso.pnatIsoNat_apply`, `IsMaxAntichain.image`, `OrderIso.coe_toRelIsoGT`, `IsLocalization.orderIsoOfPrime_symm_apply_coe`, `Subfield.extendScalars.orderIso_apply`, `OrderIso.funUnique_apply`, `Fin.castOrderIso_symm_apply`, `Con.orderIsoOp_apply`, `TwoSidedIdeal.orderIsoMatrix_symm_apply_ringCon_r`, `map_rel_iff`, `SimpleGraph.Iso.boxProdSumDistrib_apply`, `AddSubgroup.opEquiv_apply`, `Subgroup.opEquiv_symm_apply`, `OrderIso.coe_symm_toRelIsoLT`, `Submonoid.opEquiv_apply`, `PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal`, `Finset.sumEquiv_apply_snd`, `mkFactorOrderIsoOfFactorDvdEquiv_symm_apply_coe`, `CategoryTheory.Subobject.mapIsoToOrderIso_symm_apply`, `AddSubgroup.orderIsoAddCon_apply`, `InitialSeg.antisymm_toFun`, `OrderEmbedding.orderIso_apply`, `SimpleGraph.Iso.degree_eq`, `AddCon.orderIsoOp_apply`, `Ordinal.enum_zero_eq_bot`, `Fin.insertNthOrderIso_apply`, `Subsemigroup.coe_toAddSubsemigroup_symm_apply`, `AddSubmonoid.coe_toSubmonoid_symm_apply`, `SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning_symm_apply`, `OrderIso.asBoolAlgAsBoolRing_apply`, `emptySumLex_symm_apply`, `Subrepresentation.subrepresentationSubmoduleOrderIso_symm_apply`, `surjective`, `CategoryTheory.Subfunctor.orderIsoSubobject_symm_apply`, `trans_apply`, `ENNReal.orderIsoIicCoe_apply_coe`, `SimpleGraph.boxProdAssoc_symm_apply`, `AddSubgroup.coe_toSubgroup_apply`, `OrderIso.inv_apply`, `image_eq_preimage_symm`, `sumLexComplLeft_apply`, `SimpleGraph.Iso.mapNeighborSet_symm_apply_coe`, `OrderIso.compl_apply`, `Fin.orderIsoSubtype_symm_apply`, `Ideal.coe_piOrderIso_symm_apply`, `Ordinal.relIso_enum'`, `SimpleGraph.Iso.sumAssoc_apply`, `OrderIso.subLeft_symm_apply`, `Subgroup.orderIsoCon_symm_apply_coe`, `Subring.opEquiv_apply`, `OrderIso.withZeroUnits_apply`, `SimpleGraph.Iso.sumBoxProdDistrib_symm_apply`, `Submonoid.coe_toAddSubmonoid_symm_apply`, `Submonoid.coe_toAddSubmonoid_apply`, `Subalgebra.opEquiv_symm_apply`, `subrelUnivIso_apply`, `Ordinal.ToType.mk_apply`, `preimage_apply`, `self_comp_symm`, `toInitialSeg_toFun`, `OrderIso.setCongr_apply`, `Submodule.orderIsoMapComapOfBijective_apply`, `Subring.opEquiv_symm_apply`, `CompleteLatticeHom.toOrderIsoRangeOfInjective_apply`, `IsAntichain.preimage_relIso`, `SimpleGraph.induceUnivIso_symm_apply_coe`, `AddSubsemigroup.opEquiv_apply`, `OrderIso.smulRightDual_symm_apply`, `ENNReal.orderIsoRpow_apply`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe`, `TwoSidedIdeal.orderIsoIsTwoSided_apply_coe`, `Ordinal.enum_inj`, `OrderHom.prodIso_symm_apply`, `Finset.sumEquiv_apply_fst`, `ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal`, `OrderIso.divLeft_symm_apply`, `OrderHom.piIso_apply`, `SimpleGraph.hasseDualIso_symm_apply`, `OrderIso.setIsotypicComponents_symm_apply`, `Subfield.extendScalars.orderIso_symm_apply_coe`, `AddSubmonoid.coe_negOrderIso_apply`, `Fin.castLEOrderIso_apply`, `Sum.Lex.toLexRelIsoLT_symm_coe`, `IsLocalization.orderIsoOfPrime_apply_coe`, `Prod.Lex.prodLexCongr_apply`, `infIccOrderIsoIccSup_symm_apply_coe`, `AddCon.orderIsoOp_symm_apply`, `Equiv.toOrderIsoSet_apply`, `range_eq`, `OrderIso.withTopCongr_symm_apply`, `Concept.swapEquiv_symm_apply`, `SimpleGraph.Iso.coe_comp`, `coe_fn_toEquiv`, `AddSubmonoid.opEquiv_symm_apply`, `Finset.orderIsoColex_symm_apply`, `Ordinal.familyOfBFamily'_enum`, `preimage_symm_apply`, `Ordinal.enum_zero_le'`, `Ordinal.toZFSetIso_symm_apply`, `PrincipalSeg.subrelIso_apply`, `coe_toRelEmbedding`, `Ordinal.familyOfBFamily_enum`, `OrderIso.asBoolAlgAsBoolRing_symm_apply`, `ENNReal.mulLeftOrderIso_apply`, `pairwise_listMap`, `CategoryTheory.Abelian.subobjectIsoSubobjectOp_symm_apply`, `Prod.Lex.prodLexAssoc_apply`, `Subrepresentation.subrepresentationSubmoduleOrderIso_apply`, `OrderIso.finsetSetFinite_apply_coe`, `Ideal.coe_piOrderIso_apply`, `StrictMono.orderIsoOfRightInverse_apply`, `Sublattice.prodEquiv_symm_apply`, `AddSubmonoid.opEquiv_apply`, `AddSubgroup.coe_toSubgroup_symm_apply`, `apply_inv_self`, `YoungDiagram.transposeOrderIso_apply`, `WithZero.val_logOrderIso_symm_apply`, `OrderIso.mulRight_apply`, `Submonoid.opEquiv_symm_apply`, `Real.sinhOrderIso_symm_apply`, `SimpleGraph.Iso.sumAssoc_symm_apply`, `IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal`, `OrderIso.toRelIsoGT_apply`, `WithZero.val_inv_logOrderIso_symm_apply`, `Finset.orderIsoColex_apply`, `eq_symm_apply`, `Ordinal.relIso_enum`, `OrderIso.mulLeft_apply`, `OrderIso.addLeft_apply`, `Subalgebra.opEquiv_apply`, `SimpleGraph.Iso.map_apply`, `SimpleGraph.boxProdComm_apply`, `SimpleGraph.Iso.comap_symm_apply`, `AddEquiv.comapAddSubgroup_symm_apply`, `coe_fn_mk`, `SimpleGraph.Iso.sumComm_symm_apply`, `Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply`, `Subsemigroup.coe_toAddSubsemigroup_apply`, `AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe`, `Subgroup.opEquiv_apply`, `Ordinal.enum_type`, `sumLexEmpty_apply`, `Ordinal.one_toType_eq`
`instInhabited` 📖	CompOp	1 math math: `default_def`
`ofSurjective` 📖	CompOp	1 math math: `ofSurjective_apply`
`ofUniqueOfIrrefl` 📖	CompOp	—
`ofUniqueOfRefl` 📖	CompOp	—
`preimage` 📖	CompOp	2 math math: `preimage_apply`, `preimage_symm_apply`
`prodLexCongr` 📖	CompOp	—
`refl` 📖	CompOp	9 math math: `cast_refl`, `one_def`, `self_trans_symm`, `refl_symm`, `refl_apply`, `symm_trans_self`, `trans_refl`, `default_def`, `refl_trans`
`relHomCongr` 📖	CompOp	2 math math: `relHomCongr_symm_apply`, `relHomCongr_apply`
`relIsoOfIsEmpty` 📖	CompOp	—
`sumLexCongr` 📖	CompOp	—
`sumLexEmpty` 📖	CompOp	2 math math: `sumLexEmpty_symm_apply`, `sumLexEmpty_apply`
`swap` 📖	CompOp	—
`toEquiv` 📖	CompOp	32 math math: `toEquiv_injective`, `OrderIso.toFun_eq_coe`, `Finset.map_truncatedInf`, `map_rel_iff'`, `Fin.insertNthOrderIso_toEquiv`, `OrderIso.coe_symm_toEquiv`, `coe_toEmbedding`, `OrderIso.mulRight_toEquiv`, `OrderIso.withBotCongr_symm_apply`, `Fin.castOrderIso_toEquiv`, `OrderIso.toEquiv_symm`, `ENNReal.mulLeftOrderIso_toEquiv`, `OrderIso.refl_toEquiv`, `OrderIso.funUnique_toEquiv`, `Sublattice.prodEquiv_toEquiv`, `OrderIso.addRight_toEquiv`, `Fin.revOrderIso_toEquiv`, `ENNReal.mulRightOrderIso_toEquiv`, `Finset.map_truncatedSup`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal`, `OrderIso.addLeft_toEquiv`, `cast_toEquiv`, `SimpleGraph.Iso.boxProdSumDistrib_toEquiv`, `Fin.consOrderIso_toEquiv`, `Fintype.finsetOrderIsoSet_toEquiv`, `Fin.snocOrderIso_toEquiv`, `OrderIso.mulLeft_toEquiv`, `Equiv.toOrderIso_toEquiv`, `OrderIso.withTopCongr_symm_apply`, `coe_fn_toEquiv`, `OrderIso.coe_toEquiv`, `SimpleGraph.Iso.sumBoxProdDistrib_toEquiv`
`toRelEmbedding` 📖	CompOp	11 math math: `relHomCongr_symm_apply`, `SimpleGraph.Iso.connectedComponentEquiv_symm_apply`, `relHomCongr_apply`, `SimpleGraph.ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map`, `SimpleGraph.ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp`, `PartOrdEmb.Iso.mk_hom`, `SimpleGraph.Iso.mapEdgeSet_apply`, `SimpleGraph.Iso.connectedComponentEquiv_apply`, `coe_toRelEmbedding`, `SimpleGraph.Iso.mapEdgeSet_symm_apply`, `PartOrdEmb.Iso.mk_inv`
`trans` 📖	CompOp	10 math math: `trans_assoc`, `self_trans_symm`, `symm_trans_apply`, `symm_trans_self`, `SimpleGraph.Iso.connectedComponentEquiv_trans`, `cast_trans`, `trans_apply`, `trans_refl`, `mul_def`, `refl_trans`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_eq_iff_eq` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike`	—	`EquivLike.apply_eq_iff_eq`
`apply_eq_iff_eq_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm`	—	`apply_symm_apply` `apply_eq_iff_eq`
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm`	—	`Equiv.right_inv`
`bijective` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `RelIso` `instFunLike`	—	`Equiv.bijective`
`cast_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `cast`	—	—
`cast_refl` 📖	mathematical	—	`cast` `refl`	—	—
`cast_symm` 📖	mathematical	—	`symm` `cast`	—	—
`cast_toEquiv` 📖	mathematical	—	`toEquiv` `cast` `Equiv.cast`	—	—
`cast_trans` 📖	mathematical	—	`trans` `cast`	—	`ext`
`coe_copy` 📖	mathematical	`DFunLike.coe` `RelIso` `instFunLike` `symm`	`copy`	—	—
`coe_fn_injective` 📖	mathematical	—	`RelIso` `DFunLike.coe` `instFunLike`	—	`DFunLike.coe_injective`
`coe_fn_mk` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`RelIso` `instFunLike`	—	—
`coe_fn_symm_mk` 📖	mathematical	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	`RelIso` `instFunLike` `symm` `Equiv.symm`	—	—
`coe_fn_toEquiv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv` `RelIso` `instFunLike`	—	—
`coe_toEmbedding` 📖	mathematical	—	`DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Equiv.toEmbedding` `toEquiv` `RelIso` `instFunLike`	—	—
`coe_toRelEmbedding` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike` `toRelEmbedding` `RelIso` `instFunLike`	—	—
`compl_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Compl.compl` `Pi.instCompl` `Prop.instCompl` `instFunLike` `compl` `EquivLike.toFunLike` `instEquivLike`	—	—
`compl_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Compl.compl` `Pi.instCompl` `Prop.instCompl` `instFunLike` `symm` `compl` `EquivLike.inv` `instEquivLike`	—	—
`copy_eq` 📖	mathematical	`DFunLike.coe` `RelIso` `instFunLike` `symm`	`copy`	—	`DFunLike.coe_injective`
`default_def` 📖	mathematical	—	`RelIso` `instInhabited` `refl`	—	—
`emptySumLex_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `emptySumLex` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.sumEmpty`	—	—
`emptySumLex_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm` `emptySumLex`	—	—
`eq_iff_eq` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike`	—	`injective`
`eq_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm`	—	`Equiv.eq_symm_apply`
`ext` 📖	—	`DFunLike.coe` `RelIso` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike`	—	`ext`
`injective` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike`	—	`Equiv.injective`
`instRelHomClass` 📖	mathematical	—	`RelHomClass` `RelIso` `instFunLike`	—	`map_rel_iff'`
`map_rel_iff` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike`	—	`map_rel_iff'`
`map_rel_iff'` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toEquiv`	—	—
`ofSurjective_apply` 📖	mathematical	`DFunLike.coe` `RelEmbedding` `RelEmbedding.instFunLike`	`RelIso` `instFunLike` `ofSurjective`	—	—
`preimage_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Order.Preimage` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `instFunLike` `preimage`	—	—
`preimage_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Order.Preimage` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `instFunLike` `symm` `preimage` `Equiv.symm`	—	—
`refl_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `refl`	—	—
`refl_symm` 📖	mathematical	—	`symm` `refl`	—	—
`refl_trans` 📖	mathematical	—	`trans` `refl`	—	—
`relHomCongr_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `RelHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `relHomCongr` `RelHom.comp` `RelEmbedding.toRelHom` `toRelEmbedding` `symm`	—	—
`relHomCongr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `RelHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `relHomCongr` `RelHom.comp` `RelEmbedding.toRelHom` `toRelEmbedding` `symm`	—	—
`rel_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm`	—	`map_rel_iff` `apply_symm_apply`
`self_comp_symm` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm`	—	`apply_symm_apply`
`self_trans_symm` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `symm_apply_apply`
`sumLexEmpty_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `sumLexEmpty` `isEmptyElim`	—	—
`sumLexEmpty_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm` `sumLexEmpty`	—	—
`surjective` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike`	—	`Equiv.surjective`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm`	—	`Equiv.left_inv`
`symm_apply_eq` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm`	—	`Equiv.symm_apply_eq`
`symm_apply_rel` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm`	—	`map_rel_iff` `apply_symm_apply`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `RelIso` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_comp_self` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm`	—	`symm_apply_apply`
`symm_symm` 📖	mathematical	—	`symm`	—	—
`symm_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm`	—	—
`symm_trans_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `symm` `trans`	—	—
`symm_trans_self` 📖	mathematical	—	`trans` `symm` `refl`	—	`ext` `apply_symm_apply`
`toEquiv_injective` 📖	mathematical	—	`RelIso` `Equiv` `toEquiv`	—	—
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `instFunLike` `trans`	—	—
`trans_assoc` 📖	mathematical	—	`trans`	—	—
`trans_refl` 📖	mathematical	—	`trans` `refl`	—	—

RelIso.IsWellOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage` 📖	mathematical	—	`IsWellOrder` `Order.Preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`RelEmbedding.isWellOrder`
`ulift` 📖	mathematical	—	`IsWellOrder` `Order.Preimage`	—	`preimage`

RelIso.Simps

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—
`symm_apply` 📖	CompOp	—

Subtype

Definitions

Name	Category	Theorems
`relEmbedding` 📖	CompOp	1 math math: `relEmbedding_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`relEmbedding_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Order.Preimage` `RelEmbedding.instFunLike` `relEmbedding`	—	—
`wellFoundedGT` 📖	mathematical	—	`WellFoundedGT`	—	`RelEmbedding.isWellFounded`
`wellFoundedLT` 📖	mathematical	—	`WellFoundedLT`	—	`RelEmbedding.isWellFounded`

WellFounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_quotient_liftOn₂'` 📖	—	`Quotient.liftOn₂'`	—	—	`wellFounded_liftOn₂'_iff`
`of_quotient_lift₂` 📖	—	—	—	—	`wellFounded_lift₂_iff`
`quotient_liftOn₂'` 📖	mathematical	—	`Quotient.liftOn₂'`	—	`wellFounded_liftOn₂'_iff`
`quotient_lift₂` 📖	—	—	—	—	`wellFounded_lift₂_iff`

(root)

Definitions

Name	Category	Theorems
`RelEmbedding` 📖	CompData	197 math math: `AddUnits.orderEmbeddingVal_apply`, `Set.chainHeight_eq_of_relEmbedding`, `PrincipalSeg.trans_apply`, `Fin.valOrderEmb_apply`, `Ordinal.typein_le_typein`, `Ordinal.mem_range_typein_iff`, `PrincipalSeg.map_succ`, `OrderEmbedding.mulRight_apply`, `Ordinal.iSup_typein_succ`, `PrincipalSeg.isLowerSet_range`, `PrincipalSeg.isMin_apply_iff`, `InitialSeg.toPrincipalSeg_apply`, `Set.principalSegIioIicOfLE_toRelEmbedding`, `RelEmbedding.coe_one`, `PrincipalSeg.mem_range_iff_rel`, `PrincipalSeg.transInitial_apply`, `Ordinal.enum_symm_apply_coe`, `PrincipalSeg.mem_range_iff_rel'`, `RelEmbedding.smul_def`, `PrincipalSeg.isSuccLimit_apply_iff`, `SimpleGraph.Embedding.sumInr_apply`, `RelEmbedding.sumLiftRelInr_apply`, `PrincipalSeg.exists_eq_iff_rel`, `SimpleGraph.Copy.topEmbedding_apply`, `PrincipalSeg.map_bot`, `IsAntichain.image_relEmbedding`, `AddLocalization.mkOrderEmbedding_apply`, `PrincipalSeg.le_iff_le`, `PrincipalSeg.mem_range_of_rel_top`, `IsChain.image_relEmbedding`, `RelEmbedding.preimage_apply`, `LieSubmodule.toSubmodule_orderEmbedding_apply`, `RelEmbedding.sumLexMap_apply`, `Ordinal.typein_top`, `SimpleGraph.completeMultipartiteGraph.topEmbedding_apply_fst`, `Localization.mkOrderEmbedding_apply`, `NonemptyInterval.toDualProdHom_apply`, `Ordinal.bfamilyOfFamily'_typein`, `RelEmbedding.sumLexInl_apply`, `RelEmbedding.injective`, `IsChain.image_relEmbedding_iff`, `SimpleGraph.Embedding.sumInl_apply`, `PrincipalSeg.isSuccPrelimit_apply_iff`, `RelEmbedding.coe_toEmbedding`, `Ordinal.liftPrincipalSeg_coe`, `PrincipalSeg.apply_covBy_apply_iff`, `Fin.natAddOrderEmb_apply`, `Units.orderEmbeddingVal_apply`, `OrderEmbedding.withTopCoe_apply`, `RelEmbedding.one_apply`, `RelEmbedding.instRelHomClass`, `Quotient.outRelEmbedding_apply`, `PrincipalSeg.monotone`, `Ordinal.typein_lt_type`, `Nat.castOrderEmbedding_apply`, `Ordinal.type_le_iff'`, `PrincipalSeg.apply_wCovBy_apply_iff`, `Ordinal.typein_lt_typein`, `HahnSeries.embDomainOrderEmbedding_apply`, `PrincipalSeg.lt_top`, `RelEmbedding.instEmbeddingLike`, `PrincipalSeg.apply_subrelIso`, `RelEmbedding.ofMonotone_coe`, `PrincipalSeg.cocone_ι_app`, `Set.principalSegIio_toRelEmbedding`, `PrincipalSeg.transRelIso_apply`, `IsWellFounded.rank_eq_typein`, `SSet.stdSimplex.nonDegenerateEquiv_apply_apply`, `RelEmbedding.coe_fn_injective`, `RelEmbedding.coe_toRelHom`, `PrincipalSeg.strictMono`, `RelEmbedding.mul_def`, `InitialSeg.eq_principalSeg`, `CategoryTheory.Functor.IsWellOrderContinuous.nonempty_isColimit`, `RelEmbedding.pairwise_swap_listMap`, `ENat.toENNRealOrderEmbedding_apply`, `RelEmbedding.prodLexMkRight_apply`, `orderEmbeddingOfInjective_apply`, `Ordinal.type_subrel`, `RelEmbedding.apply_faithfulSMul`, `RelEmbedding.pairwise_listMap`, `PrincipalSeg.ext_iff`, `RelEmbedding.sumLexInr_apply`, `Set.wellFoundedOn_iff_no_descending_seq`, `Ordinal.enum_typein`, `RelEmbedding.sumLiftRelMap_apply`, `Subrel.relEmbedding_apply`, `PrincipalSeg.trans_top`, `Cardinal.card_typein_lt`, `Cardinal.card_typein_toType_lt`, `OrderEmbedding.withTopMap_apply`, `Ordinal.blsub_type`, `PrincipalSeg.coe_coe_fn'`, `PrincipalSeg.relIsoTrans_apply`, `RelEmbedding.coe_trans`, `RelEmbedding.map_rel_iff`, `PrincipalSeg.cocone_pt`, `Finsupp.orderEmbeddingToFun_apply`, `PrincipalSeg.orderIsoIio_apply_coe`, `PrincipalSeg.lt_apply_iff`, `PrincipalSeg.ofElement_apply`, `SSet.orderEmbeddingN_apply`, `Ordinal.bfamilyOfFamily_typein`, `Ordinal.typein_enum`, `PrincipalSeg.subrelIso_symm_apply`, `PrincipalSeg.map_isSuccPrelimit`, `Ordinal.typein_surj`, `Ordinal.typein_injective`, `RelEmbedding.inj`, `RelEmbedding.eq_preimage`, `RelEmbedding.refl_apply`, `Rat.castOrderEmbedding_apply`, `Ordinal.typein_apply`, `Ordinal.ToType.mk_symm_apply_coe`, `InitialSeg.transPrincipal_apply`, `Field.Emb.Cardinal.filtration_apply`, `PrincipalSeg.toRelEmbedding_injective`, `PrimeSpectrum.nhdsOrderEmbedding_apply`, `Ordinal.typein_surjOn`, `OrderEmbedding.withBotCoe_apply`, `RelEmbedding.sumLiftRelInl_apply`, `OrderEmbedding.addRight_apply`, `Ordinal.iSup_typein_limit`, `RelEmbedding.ofMapRelIff_coe`, `PrincipalSeg.isNormal`, `Ordinal.card_typein`, `Ordinal.lift_typein_top`, `RelEmbedding.prodLexMap_apply`, `Ordinal.typein_ordinal`, `RelEmbedding.coe_natLT`, `RelEmbedding.acc_iff_isEmpty_subtype_mem_range`, `OrderEmbedding.gtEmbedding_apply`, `WithTop.coeOrderHom_apply`, `RelEmbedding.coe_natGT`, `Ordinal.lsub_typein`, `OrderEmbedding.orderIso_apply`, `Multiset.mapEmbedding_apply`, `RelEmbedding.ext_iff`, `PrincipalSeg.surjOn`, `OrderEmbedding.addLeft_apply`, `PrincipalSeg.acc`, `Fin.castSuccOrderEmb_apply`, `Ordinal.typein_lt_self`, `SimpleGraph.completeMultipartiteGraph.topEmbedding_apply_snd`, `PrincipalSeg.map_isSuccLimit`, `RelEmbedding.toEmbedding_injective`, `RelEmbedding.orderEmbeddingOfLTEmbedding_apply`, `PrincipalSeg.eq`, `LieSubmodule.mapOrderEmbedding_apply`, `TwoSidedIdeal.coeOrderEmbedding_apply`, `RelEmbedding.not_acc`, `WithBot.coeOrderHom_apply`, `Ordinal.typein_one_toType`, `RelEmbedding.sorted_listMap`, `CompleteLatticeHom.toOrderIsoRangeOfInjective_apply`, `Ordinal.sup_typein_limit`, `RelEmbedding.mul_apply`, `CategoryTheory.SmallObject.restrictionLT_map`, `Ordinal.typein_le_typein'`, `OrderEmbedding.ltEmbedding_apply`, `RelEmbedding.coe_mul`, `Subtype.orderEmbedding_apply_coe`, `SimpleGraph.boxProdRight_apply`, `CategoryTheory.SmallObject.coconeOfLE_ι_app`, `RelEmbedding.one_def`, `RelEmbedding.sorted_swap_listMap`, `IsChain.preimage_relEmbedding`, `RelEmbedding.prodLexMkLeft_apply`, `Submodule.restrictScalarsEmbedding_apply`, `OrderEmbedding.ofAntisymmetrization_apply`, `IsAntichain.preimage_relEmbedding`, `Ordinal.typein_inj`, `PrincipalSeg.subrelIso_apply`, `RelIso.coe_toRelEmbedding`, `Subtype.relEmbedding_apply`, `OrderEmbedding.withBotMap_apply`, `RelEmbedding.coe_mk`, `IsAntichain.image_relEmbedding_iff`, `PrincipalSeg.le_apply_iff`, `Fin.castLEOrderEmb_apply`, `Subrel.coe_inclusionEmbedding`, `InitialSeg.coe_coe_fn`, `Fin.castAddOrderEmb_apply`, `OrderEmbedding.ofIsEmpty_apply`, `RelEmbedding.wellFounded_iff_isEmpty`, `SimpleGraph.boxProdLeft_apply`, `Ordinal.toPGameEmbedding_apply`, `NNRat.castOrderEmbedding_apply`, `RelEmbedding.trans_apply`, `OrderEmbedding.mulLeft_apply`, `PrincipalSeg.map_isMin`, `PrincipalSeg.image_Iio`, `Ordinal.sup_typein_succ`, `Fin.addNatOrderEmb_apply`, `Fin.succAboveOrderEmb_apply`, `PrincipalSeg.lt_iff_lt`, `RelEmbedding.swap_apply`
`RelHom` 📖	CompData	30 math math: `SimpleGraph.homOfConnectedComponents_apply`, `RelHom.one_def`, `RelIso.relHomCongr_symm_apply`, `RelHom.swap_apply`, `RelHom.one_apply`, `RelHom.coeFn_mk`, `RelHom.mul_apply`, `RelIso.relHomCongr_apply`, `RelHom.instRelHomClass`, `RelEmbedding.coe_toRelHom`, `RelHom.coe_fn_injective`, `RelHom.coe_fn_toFun`, `RelHom.toOrderHom_coe`, `SimpleGraph.Hom.comap_apply`, `RelHom.coe_one`, `Quotient.mkRelHom_apply`, `RelHom.preimage_apply`, `SimpleGraph.induceHom_comp`, `RelHom.smul_def`, `RelHom.mul_def`, `SimpleGraph.Subgraph.spanningHom_apply`, `RelHom.comp_apply`, `RelHom.map_rel`, `SimpleGraph.Subgraph.inclusion_apply_coe`, `SimpleGraph.Subgraph.hom_apply`, `RelHom.apply_faithfulSMul`, `RelHom.injective_of_increasing`, `RelHom.id_apply`, `RelHom.ext_iff`, `RelHom.coe_mul`
`RelHomClass` 📖	CompData	8 math math: `InitialSeg.instRelHomClass`, `PseudoEpimorphismClass.toRelHomClass`, `RelEmbedding.instRelHomClass`, `BoundedOrderHomClass.toRelHomClass`, `CompactExhaustion.instRelHomClassNatSetLeSubset`, `RelHom.instRelHomClass`, `RelIso.instRelHomClass`, `Set.FiniteExhaustion.instRelHomClassNatLeSubset`
`RelIso` 📖	CompData	364 math math: `IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal`, `WithZero.logOrderIso_apply`, `TwoSidedIdeal.orderIsoRingCon_symm_apply`, `Ordinal.type_eq`, `WithZero.val_expOrderIso_apply`, `ULift.orderIso_symm_apply_down`, `YoungDiagram.transposeOrderIso_symm_apply`, `RelIso.one_apply`, `OrderIso.arrowCongr_apply`, `OrderIso.sumCongr_apply`, `Subgroup.MapSubtype.orderIso_apply_coe`, `OrderIso.withTopCongr_apply`, `Submonoid.coe_invOrderIso_apply`, `IsLocalization.AtPrime.coe_orderIsoOfPrime_apply_coe`, `RingEquiv.idealComapOrderIso_apply`, `RelIso.toEquiv_injective`, `Ordinal.isInitialIso_apply`, `RelIso.sumLexComplRight_apply`, `RelIso.smul_def`, `OrderIso.mulRight₀_symm_apply`, `OrderIso.smulRight_apply`, `TopologicalSpace.Closeds.complOrderIso_symm_apply`, `PrimeSpectrum.equivSubtype_apply_coe`, `AddSubsemigroup.coe_toSubsemigroup_symm_apply`, `upperSetIsoLowerSet_apply`, `OrderIso.toRelIsoLT_apply`, `PrimeSpectrum.equivSubtype_symm_apply_asIdeal`, `IsMaxChain.image`, `TwoSidedIdeal.orderIsoRingCon_apply`, `OrderIso.divRight_symm_apply`, `OrderIso.neg_apply`, `ENNReal.mulRightOrderIso_symm_apply`, `RelIso.coe_fn_symm_mk`, `OrderHom.piIso_symm_apply`, `IsAntichain.image_relIso_iff`, `Ordinal.enum_symm_apply_coe`, `PrincipalSeg.transRelIso_top`, `MulEquiv.comapSubgroup_symm_apply`, `Ordinal.enum_zero_le`, `Submonoid.coe_invOrderIso_symm_apply`, `RelIso.sumLexComplLeft_symm_apply`, `IsChain.image_relIso`, `Ordinal.enum_lt_enum`, `NNReal.orderIsoRpow_apply`, `Ordinal.isInitialIso_symm_apply_coe`, `OrderIso.subLeft_apply`, `Subsemigroup.opEquiv_symm_apply`, `RelIso.preimage_eq_image_symm`, `IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal`, `RelIso.mul_apply`, `TopologicalSpace.Opens.complOrderIso_apply`, `RelIso.eq_iff_eq`, `Homeomorph.opensCongr_apply`, `OrderIso.inv_symm_apply`, `OrderIso.addRight_apply`, `AddSubmonoid.coe_toSubmonoid_apply`, `SimpleGraph.Iso.sumComm_apply`, `OrderHom.prodIso_apply`, `AddSubsemigroup.coe_toSubsemigroup_apply`, `StrictMono.orderIso_apply`, `TwoSidedIdeal.orderIsoMatrix_apply_ringCon_r`, `IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe`, `OrderIso.prodAssoc_apply`, `SimpleGraph.Iso.sumBoxProdDistrib_apply`, `TopologicalSpace.Opens.complOrderIso_symm_apply`, `RelIso.one_def`, `MulEquiv.mapSubgroup_apply`, `OrderIso.mulRight₀_apply`, `Equiv.toOrderIsoSet_symm_apply`, `RelIso.cast_apply`, `LieSubmodule.orderIsoMapComap_apply`, `SimpleGraph.induceUnivIso_apply`, `OrderIso.smulRightDual_apply`, `Fin.revOrderIso_apply`, `Prod.Lex.prodLexAssoc_symm_apply`, `OrderIso.setIsotypicComponents_apply`, `WithZero.expOrderIso_symm_apply`, `IsLocalization.AtPrime.coe_primeSpectrumOrderIso_apply_coe_asIdeal`, `Ordinal.enum_le_enum'`, `PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal`, `Fin.insertNthOrderIso_symm_apply`, `InitialSeg.eq_relIso`, `Ordinal.lift_type_eq`, `RelIso.symm_bijective`, `OrderIso.ofRelIsoLT_apply`, `RelIso.emptySumLex_apply`, `OrderIso.divRight₀_symm_apply`, `OrderIso.mulLeft₀_apply`, `IsGalois.intermediateFieldEquivSubgroup_apply`, `RelIso.bijective`, `CategoryTheory.Abelian.subobjectIsoSubobjectOp_apply`, `OrderIso.finsetSetFinite_symm_apply`, `RelIso.coe_toEmbedding`, `TwoSidedIdeal.orderIsoIsTwoSided_symm_apply`, `TwoSidedIdeal.opOrderIso_symm_apply`, `OrderIso.divLeft_apply`, `OrderIso.coe_toRelIsoLT`, `RelIso.coe_one`, `Prod.Lex.sumLexProdLexDistrib_symm_apply`, `Sum.Lex.toLexRelIsoLE_coe`, `RelIso.coe_mul`, `OrderIso.subRight_symm_apply`, `RelIso.ext_iff`, `IsChain.image_relIso_iff`, `OrderIso.withBotCongr_symm_apply`, `Subsemiring.opEquiv_apply`, `upperSetIsoLowerSet_symm_apply`, `ENNReal.orderIsoIicOneBirational_apply_coe`, `IntermediateField.extendScalars.orderIso_apply`, `RelIso.symm_apply_eq`, `OrderIso.withZeroUnits_symm_apply`, `TopologicalSpace.Closeds.complOrderIso_apply`, `InitialSeg.exists_sum_relIso`, `OrderIso.ofHomInv_apply`, `LieSubmodule.orderIsoMapComap_symm_apply`, `AddSubsemigroup.opEquiv_symm_apply`, `infIccOrderIsoIccSup_apply_coe`, `RelIso.sumLexEmpty_symm_apply`, `ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier`, `PrincipalSeg.apply_subrelIso`, `RelIso.subrelUnivIso_symm_apply`, `RelIso.coe_fn_injective`, `StrictMono.orderIsoOfRightInverse_symm_apply`, `SimpleGraph.boxProdComm_symm_apply`, `OrderIso.setCongr_symm_apply`, `OrderIso.smulRight_symm_apply`, `PrincipalSeg.transRelIso_apply`, `RelIso.compl_apply`, `infIooOrderIsoIooSup_symm_apply_coe`, `CategoryTheory.Subobject.mapIsoToOrderIso_apply`, `AddSubmonoid.coe_negOrderIso_symm_apply`, `Con.orderIsoOp_symm_apply`, `Subrepresentation.submoduleSubrepresentationOrderIso_apply`, `RelIso.instRelHomClass`, `RelIso.symm_apply_apply`, `SimpleGraph.boxProdAssoc_apply`, `ENNReal.mulRightOrderIso_apply`, `RelIso.rel_symm_apply`, `AddEquiv.mapAddSubgroup_symm_apply`, `Subgroup.coe_toAddSubgroup_symm_apply`, `Fin.castOrderIso_apply`, `Sum.Lex.toLexRelIsoLE_symm_coe`, `Prod.Lex.sumLexProdLexDistrib_apply`, `OrderIso.arrowCongr_symm_apply`, `IsAntichain.image_relIso`, `Sublattice.prodEquiv_apply`, `RingCon.opOrderIso_apply`, `mkFactorOrderIsoOfFactorDvdEquiv_apply_coe`, `WithZero.val_inv_expOrderIso_apply`, `OrderIso.compl_symm_apply`, `OrderIso.prodAssoc_symm_apply`, `TwoSidedIdeal.opOrderIso_apply`, `IsChain.preimage_relIso`, `RelIso.apply_eq_iff_eq`, `RelIso.inv_apply_self`, `OrderIso.sumLexCongr_apply`, `Concept.swapEquiv_apply`, `Subgroup.orderIsoCon_apply`, `OrderIso.ofUnique_symm_apply`, `RelIso.apply_eq_iff_eq_symm_apply`, `Ordinal.le_enum_succ`, `ENNReal.mulLeftOrderIso_symm_apply`, `Fin.snocOrderIso_apply`, `RelIso.symm_apply_rel`, `AddEquiv.comapAddSubgroup_apply`, `Ordinal.enum_typein`, `RelIso.injective`, `Set.chainHeight_eq_of_relIso`, `RelIso.symm_comp_self`, `OrderIso.divRight₀_apply`, `SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning_apply_coe`, `AddSubgroup.orderIsoAddCon_symm_apply_coe`, `MulEquiv.mapSubgroup_symm_apply`, `RelIso.symm_symm_apply`, `PrincipalSeg.relIsoTrans_apply`, `CategoryTheory.Subfunctor.orderIsoSubobject_apply`, `RelIso.ofSurjective_apply`, `Fin.orderIsoSubtype_apply`, `Submodule.orderIsoMapComapOfBijective_symm_apply`, `Fin.snocOrderIso_symm_apply`, `OrderIso.divRight_apply`, `RelIso.apply_faithfulSMul`, `Subsemiring.opEquiv_symm_apply`, `PrincipalSeg.orderIsoIio_apply_coe`, `Fin.consOrderIso_apply`, `ULift.orderIso_apply`, `Ordinal.typein_enum`, `AddSubgroup.opEquiv_symm_apply`, `OrderIso.ofUnique_apply`, `PrincipalSeg.subrelIso_symm_apply`, `Real.sinhOrderIso_apply`, `OrderIso.subRight_apply`, `AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_apply_coe_coe`, `RelIso.sumLexComplRight_symm_apply`, `Ordinal.toZFSetIso_apply`, `RelIso.pairwise_swap_listMap`, `PrimeSpectrum.comapEquiv_apply`, `MulEquiv.comapSubgroup_apply`, `AddSubgroup.MapSubtype.orderIso_apply_coe`, `OrderIso.withBotCongr_apply`, `Ordinal.ToType.mk_symm_apply_coe`, `Subgroup.coe_toAddSubgroup_apply`, `Submodule.orderIsoMapComap_apply`, `RelIso.refl_apply`, `RelIso.apply_symm_apply`, `Ordinal.enum_succ_eq_top`, `OrderIso.coe_symm_toRelIsoGT`, `RelIso.compl_symm_apply`, `OrderIso.sumComm_apply`, `RelIso.symm_trans_apply`, `OrderIso.neg_symm_apply`, `RingCon.opOrderIso_symm_apply`, `Fin.castLEOrderIso_symm_apply`, `Fin.consOrderIso_symm_apply`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal`, `OrderIso.invENNReal_apply`, `Subsemigroup.opEquiv_apply`, `SimpleGraph.Iso.boxProdSumDistrib_symm_apply`, `infIooOrderIsoIooSup_apply_coe`, `IntermediateField.extendScalars.orderIso_symm_apply_coe`, `AddEquiv.mapAddSubgroup_apply`, `OrderIso.mulLeft₀_symm_apply`, `Sum.Lex.toLexRelIsoLT_coe`, `Ordinal.enum_le_enum`, `OrderIso.pnatIsoNat_apply`, `IsMaxAntichain.image`, `OrderIso.coe_toRelIsoGT`, `IsLocalization.orderIsoOfPrime_symm_apply_coe`, `Subfield.extendScalars.orderIso_apply`, `OrderIso.funUnique_apply`, `Fin.castOrderIso_symm_apply`, `Con.orderIsoOp_apply`, `TwoSidedIdeal.orderIsoMatrix_symm_apply_ringCon_r`, `RelIso.map_rel_iff`, `SimpleGraph.Iso.boxProdSumDistrib_apply`, `AddSubgroup.opEquiv_apply`, `Subgroup.opEquiv_symm_apply`, `OrderIso.coe_symm_toRelIsoLT`, `Submonoid.opEquiv_apply`, `PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal`, `Finset.sumEquiv_apply_snd`, `mkFactorOrderIsoOfFactorDvdEquiv_symm_apply_coe`, `CategoryTheory.Subobject.mapIsoToOrderIso_symm_apply`, `AddSubgroup.orderIsoAddCon_apply`, `InitialSeg.antisymm_toFun`, `OrderEmbedding.orderIso_apply`, `AddCon.orderIsoOp_apply`, `Ordinal.enum_zero_eq_bot`, `Fin.insertNthOrderIso_apply`, `Subsemigroup.coe_toAddSubsemigroup_symm_apply`, `AddSubmonoid.coe_toSubmonoid_symm_apply`, `SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning_symm_apply`, `OrderIso.asBoolAlgAsBoolRing_apply`, `RelIso.emptySumLex_symm_apply`, `Subrepresentation.subrepresentationSubmoduleOrderIso_symm_apply`, `RelIso.surjective`, `CategoryTheory.Subfunctor.orderIsoSubobject_symm_apply`, `RelIso.trans_apply`, `ENNReal.orderIsoIicCoe_apply_coe`, `SimpleGraph.boxProdAssoc_symm_apply`, `AddSubgroup.coe_toSubgroup_apply`, `OrderIso.inv_apply`, `RelIso.image_eq_preimage_symm`, `RelIso.sumLexComplLeft_apply`, `OrderIso.compl_apply`, `OrderHom.curry_symm_apply`, `Fin.orderIsoSubtype_symm_apply`, `Ideal.coe_piOrderIso_symm_apply`, `Ordinal.relIso_enum'`, `SimpleGraph.Iso.sumAssoc_apply`, `OrderIso.subLeft_symm_apply`, `Subgroup.orderIsoCon_symm_apply_coe`, `Subring.opEquiv_apply`, `OrderIso.withZeroUnits_apply`, `SimpleGraph.Iso.sumBoxProdDistrib_symm_apply`, `Submonoid.coe_toAddSubmonoid_symm_apply`, `Submonoid.coe_toAddSubmonoid_apply`, `Subalgebra.opEquiv_symm_apply`, `RelIso.subrelUnivIso_apply`, `Ordinal.ToType.mk_apply`, `RelIso.preimage_apply`, `RelIso.self_comp_symm`, `RelIso.toInitialSeg_toFun`, `OrderIso.setCongr_apply`, `Submodule.orderIsoMapComapOfBijective_apply`, `Subring.opEquiv_symm_apply`, `CompleteLatticeHom.toOrderIsoRangeOfInjective_apply`, `IsAntichain.preimage_relIso`, `SimpleGraph.induceUnivIso_symm_apply_coe`, `AddSubsemigroup.opEquiv_apply`, `OrderIso.smulRightDual_symm_apply`, `ENNReal.orderIsoRpow_apply`, `PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe`, `TwoSidedIdeal.orderIsoIsTwoSided_apply_coe`, `RelIso.mul_def`, `Ordinal.enum_inj`, `RelIso.default_def`, `OrderHom.prodIso_symm_apply`, `Finset.sumEquiv_apply_fst`, `ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal`, `OrderIso.divLeft_symm_apply`, `OrderHom.piIso_apply`, `OrderIso.setIsotypicComponents_symm_apply`, `Subfield.extendScalars.orderIso_symm_apply_coe`, `AddSubmonoid.coe_negOrderIso_apply`, `Fin.castLEOrderIso_apply`, `Sum.Lex.toLexRelIsoLT_symm_coe`, `IsLocalization.orderIsoOfPrime_apply_coe`, `Prod.Lex.prodLexCongr_apply`, `infIccOrderIsoIccSup_symm_apply_coe`, `AddCon.orderIsoOp_symm_apply`, `Equiv.toOrderIsoSet_apply`, `RelIso.range_eq`, `OrderIso.withTopCongr_symm_apply`, `Concept.swapEquiv_symm_apply`, `RelIso.coe_fn_toEquiv`, `AddSubmonoid.opEquiv_symm_apply`, `Finset.orderIsoColex_symm_apply`, `Ordinal.familyOfBFamily'_enum`, `RelIso.preimage_symm_apply`, `Ordinal.enum_zero_le'`, `Ordinal.toZFSetIso_symm_apply`, `PrincipalSeg.subrelIso_apply`, `RelIso.coe_toRelEmbedding`, `Ordinal.familyOfBFamily_enum`, `OrderIso.asBoolAlgAsBoolRing_symm_apply`, `ENNReal.mulLeftOrderIso_apply`, `RelIso.pairwise_listMap`, `CategoryTheory.Abelian.subobjectIsoSubobjectOp_symm_apply`, `Prod.Lex.prodLexAssoc_apply`, `Subrepresentation.subrepresentationSubmoduleOrderIso_apply`, `OrderIso.finsetSetFinite_apply_coe`, `Ideal.coe_piOrderIso_apply`, `StrictMono.orderIsoOfRightInverse_apply`, `Sublattice.prodEquiv_symm_apply`, `AddSubmonoid.opEquiv_apply`, `AddSubgroup.coe_toSubgroup_symm_apply`, `RelIso.apply_inv_self`, `YoungDiagram.transposeOrderIso_apply`, `WithZero.val_logOrderIso_symm_apply`, `OrderIso.mulRight_apply`, `Submonoid.opEquiv_symm_apply`, `Real.sinhOrderIso_symm_apply`, `SimpleGraph.Iso.sumAssoc_symm_apply`, `IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal`, `OrderIso.toRelIsoGT_apply`, `WithZero.val_inv_logOrderIso_symm_apply`, `Finset.orderIsoColex_apply`, `RelIso.eq_symm_apply`, `Ordinal.relIso_enum`, `OrderIso.mulLeft_apply`, `OrderIso.addLeft_apply`, `Subalgebra.opEquiv_apply`, `SimpleGraph.boxProdComm_apply`, `AddEquiv.comapAddSubgroup_symm_apply`, `RelIso.coe_fn_mk`, `SimpleGraph.Iso.sumComm_symm_apply`, `Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply`, `Subsemigroup.coe_toAddSubsemigroup_apply`, `AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv_symm_apply_coe`, `Subgroup.opEquiv_apply`, `Ordinal.enum_type`, `RelIso.sumLexEmpty_apply`, `Ordinal.one_toType_eq`
`«term_→r_»` 📖	CompOp	—
`«term_↪r_»` 📖	CompOp	—
`«term_≃r_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acc_liftOn₂'_iff` 📖	mathematical	—	`Quotient.liftOn₂'` `Quotient.mk''`	—	`acc_lift₂_iff`
`acc_lift₂_iff` 📖	—	—	—	—	`RelHomClass.acc` `RelHom.instRelHomClass`
`injective_of_increasing` 📖	—	—	—	—	`trichotomous_of` `irrefl_of`
`preimage_equivalence` 📖	mathematical	—	`Order.Preimage`	—	—
`wellFounded_liftOn₂'_iff` 📖	mathematical	—	`Quotient.liftOn₂'`	—	`wellFounded_lift₂_iff`
`wellFounded_lift₂_iff` 📖	—	—	—	—	`RelHomClass.wellFounded` `RelHom.instRelHomClass` `acc_lift₂_iff`

---

← Back to Index