Basic

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

Statistics

Metric	Count
Definitions instInhabitedOrderEmbeddingNat, addNatOrderEmb, castAddOrderEmb, castLEOrderEmb, castOrderIso, castSuccOrderEmb, instBiheytingAlgebra, instBoundedOrder, instCoheytingAlgebra, instHeytingAlgebra, instLattice, instLinearOrder, instMax_mathlib, instMin_mathlib, instPartialOrder, natAddOrderEmb, orderIsoSubtype, predAboveOrderHom, revOrderIso, succAboveOrderEmb, succOrderEmb, valOrderEmb	22
Theorems isWellOrder, default_def, addNatOrderEmb_apply, addNatOrderEmb_toEmbedding, addNat_inj, addNat_le_addNat_iff, addNat_lt_addNat_iff, antitone_iff_succ_le, bot_eq_zero, castAddOrderEmb_apply, castAddOrderEmb_toEmbedding, castLEOrderEmb_apply, castLEOrderEmb_toEmbedding, castLE_le_castLE_iff, castLE_lt_castLE_iff, castOrderIso_apply, castOrderIso_refl, castOrderIso_symm_apply, castOrderIso_toEquiv, castSuccOrderEmb_apply, castSuccOrderEmb_toEmbedding, cast_strictMono, cast_top, coe_max, coe_min, coe_orderIso_apply, coe_succOrderEmb, compare_eq_compare_val, monotone_castPred_comp, monotone_iff_le_succ, monotone_pred_comp, natAddOrderEmb_apply, natAddOrderEmb_toEmbedding, natAdd_inj, natAdd_injective, natAdd_le_natAdd_iff, natAdd_lt_natAdd_iff, orderHom_injective_iff, orderIsoSubtype_apply, orderIsoSubtype_symm_apply, predAboveOrderHom_coe, predAbove_le_predAbove, predAbove_left_inj, predAbove_left_injective, predAbove_left_monotone, predAbove_right_monotone, revOrderIso_apply, revOrderIso_symm_apply, revOrderIso_toEquiv, rev_anti, rev_bot, rev_last_eq_bot, rev_strictAnti, rev_top, rev_zero_eq_top, strictAnti_iff_succ_lt, strictMono_addNat, strictMono_castAdd, strictMono_castLE, strictMono_castPred_comp, strictMono_castSucc, strictMono_iff_lt_succ, strictMono_natAdd, strictMono_pred_comp, strictMono_succ, strictMono_succAbove, succAboveOrderEmb_apply, succAboveOrderEmb_toEmbedding, succAbove_inj, succAbove_le_succAbove_iff, succAbove_lt_succAbove_iff, succOrderEmb_toEmbedding, succ_top, symm_castOrderIso, top_eq_last, top_eq_zero, valOrderEmb_apply, val_strictMono, val_top, zero_eq_top	80
Total	102

Fin

Definitions

Name	Category	Theorems
addNatOrderEmb 📖	CompOp	2 math math: addNatOrderEmb_toEmbedding, addNatOrderEmb_apply
castAddOrderEmb 📖	CompOp	2 math math: castAddOrderEmb_toEmbedding, castAddOrderEmb_apply
castLEOrderEmb 📖	CompOp	2 math math: castLEOrderEmb_toEmbedding, castLEOrderEmb_apply
castOrderIso 📖	CompOp	8 math math: AugmentedSimplexCategory.eqToHom_toOrderHom, symm_castOrderIso, castOrderIso_toEquiv, castOrderIso_apply, SimplexCategory.eqToHom_toOrderHom, castOrderIso_symm_apply, castOrderIso_refl, Finset.orderEmbOfFin_compl_singleton
castSuccOrderEmb 📖	CompOp	2 math math: castSuccOrderEmb_toEmbedding, castSuccOrderEmb_apply
instBiheytingAlgebra 📖	CompOp	—
instBoundedOrder 📖	CompOp	—
instCoheytingAlgebra 📖	CompOp	10 math math: top_eq_last, rev_top, top_eq_zero, cast_top, rev_zero_eq_top, range_natAdd_eq_Ioi, val_top, zero_eq_top, rev_bot, succ_top
instHeytingAlgebra 📖	CompOp	13 math math: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, rev_top, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F, bot_eq_zero, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_F, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot, rev_last_eq_bot, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom, rev_bot
instLattice 📖	CompOp	46 math math: image_castSucc_uIcc, prod_uIcc_cast, preimage_addNat_uIcc_addNat, finsetImage_castAdd_uIcc, finsetImage_castSucc_uIcc, map_castLEEmb_uIcc, map_valEmbedding_uIcc, map_succEmb_uIcc, card_uIcc, map_natAddEmb_uIcc, preimage_val_uIcc_val, preimage_castSucc_uIcc_castSucc, preimage_succ_uIcc_succ, prod_uIcc_castLE, finsetImage_succ_uIcc, map_finCongr_uIcc, finsetImage_castLE_uIcc, finsetImage_rev_uIcc, prod_uIcc_castSucc, attachFin_uIcc, preimage_natAdd_uIcc_natAdd, map_revPerm_uIcc, map_addNatEmb_uIcc, sum_uIcc_castAdd, map_castAddEmb_uIcc, image_addNat_uIcc, map_castSuccEmb_uIcc, image_succ_uIcc, image_val_uIcc, sum_uIcc_castSucc, image_natAdd_uIcc, sum_uIcc_castLE, finsetImage_natAdd_uIcc, prod_uIcc_succ, finsetImage_val_uIcc, prod_uIcc_castAdd, preimage_castAdd_uIcc_castAdd, preimage_cast_uIcc, preimage_rev_uIcc, finsetImage_cast_uIcc, image_castLE_uIcc, sum_uIcc_cast, finsetImage_addNat_uIcc, preimage_castLE_uIcc_castLE, image_castAdd_uIcc, sum_uIcc_succ
instLinearOrder 📖	CompOp	81 math math: Composition.orderEmbOfFin_boundaries, addNatOrderEmb_toEmbedding, SSet.horn₃₁.desc.multicofork_π_two, preimage_castSucc_uIoo_castSucc, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, image_addNat_uIoc, preimage_natAdd_uIoo_natAdd, image_castLE_uIoc, SSet.horn₃₂.desc.multicofork_π_one, MvPolynomial.supDegree_esymmAlgHomMonomial, image_succ_uIoo, Tuple.sort_perm, preimage_castSucc_uIoc_castSucc, castSuccOrderEmb_toEmbedding, preimage_castLE_uIoc_castLE, preimage_natAdd_uIoc_natAdd, natAddOrderEmb_toEmbedding, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isColimit_desc, MultilinearMap.curryFinFinset_apply, SSet.horn₃₁.desc.multicofork_pt, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_F, preimage_addNat_uIoc_addNat, MvPolynomial.leadingCoeff_esymmAlgHomMonomial, image_val_uIoo, preimage_cast_uIoo, SSet.horn₃₁.desc.multicofork_π_two_assoc, SSet.horn₃₁.desc.multicofork_π_zero_assoc, SSet.stdSimplex.nonDegenerateEquiv_apply_apply, Affine.Simplex.face_points, preimage_castAdd_uIoo_castAdd, MvPolynomial.supDegree_esymm, castLEOrderEmb_toEmbedding, preimage_val_uIoo_val, MvPolynomial.monic_esymm, Finset.orderEmbOfFin_compl_singleton_eq_succAboveOrderEmb, image_castLE_uIoo, castAddOrderEmb_toEmbedding, image_castAdd_uIoo, image_castAdd_uIoc, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_F, succAboveOrderEmb_toEmbedding, SSet.horn₃₂.desc.multicofork_π_zero_assoc, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv, preimage_cast_uIoc, image_castSucc_uIoo, image_natAdd_uIoo, preimage_succ_uIoc_succ, sort_univ, preimage_val_uIoc_val, SSet.horn₃₁.desc.multicofork_π_three_assoc, SSet.horn₃₁.desc.multicofork_π_zero, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isoBot, SSet.horn₃₂.desc.multicofork_π_three, image_addNat_uIoo, SimplexCategory.toCat_obj, SimplexCategory.skeletalFunctor_obj, preimage_addNat_uIoo_addNat, SSet.horn₃₂.desc.multicofork_pt, preimage_rev_uIoo, image_val_uIoc, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, SimplexCategory.skeletalFunctor_map, preimage_castAdd_uIoc_castAdd, ContinuousMultilinearMap.curryFinFinset_symm_apply, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit, MultilinearMap.curryFinFinset_symm_apply, Affine.Simplex.face_points', SimplexCategory.toCat_map, SSet.horn₃₂.desc.multicofork_π_zero, SSet.horn₃₂.desc.multicofork_π_three_assoc, SSet.horn₃₂.desc.multicofork_π_one_assoc, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_hom, image_succ_uIoc, preimage_castLE_uIoo_castLE, ContinuousMultilinearMap.curryFinFinset_apply, SSet.horn₃₁.desc.multicofork_π_three, image_natAdd_uIoc, preimage_succ_uIoo_succ, Finset.orderEmbOfFin_compl_singleton_apply, Finset.orderEmbOfFin_compl_singleton, image_castSucc_uIoc
instMax_mathlib 📖	CompOp	2 math math: attachFin_uIcc, coe_max
instMin_mathlib 📖	CompOp	1 math math: coe_min
instPartialOrder 📖	CompOp	710 math math: SSet.OneTruncation₂.nerveEquiv_apply, CategoryTheory.Triangulated.SpectralObject.Hom.comm, HomotopyCategory.spectralObjectMappingCone_δ'_app, finsetImage_castLE_Iio, image_addNat_Ioo, image_castLE_Ioo, card_Ioi, CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, CategoryTheory.ComposableArrows.threeδ₂Toδ₁_app_zero, CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_inv_app, CategoryTheory.ComposableArrows.exact_iff_δlast, preimage_natAdd_Iio_natAdd, map_succEmb_Iio, CategoryTheory.ComposableArrows.sc'MapIso_inv, finsetImage_natAdd_Ioc, SSet.stdSimplex.mem_nonDegenerate_iff_strictMono, SSet.stdSimplex.coe_triangle_down_toOrderHom, SimplexCategory.eq_const_of_zero, addNatOrderEmb_toEmbedding, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id_assoc, image_castLE_Icc, Ioi_succ, CategoryTheory.nerve.σ_obj, preimage_val_Ici_val, CategoryTheory.ShortComplex.mapToComposableArrows_app_0, CategoryTheory.ComposableArrows.IsComplex.zero'_assoc, isAddFreimanIso_Iio, Ico_add_one_eq_Ioo, map_castLEEmb_Ioc, finsetImage_castLE_Ioo, preimage_castAdd_Ico_castAdd, CategoryTheory.ComposableArrows.isIso_iff₂, map_revPerm_Ioc, image_val_Iic, map_castAddEmb_Ico, predAbove_left_monotone, CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_zero, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_distinguished, finsetImage_addNat_Ioi, attachFin_Iic, CategoryTheory.nerve.δ₂_zero, preimage_natAdd_Ioi_natAdd, CategoryTheory.instMonoMap'KernelCokernelCompSequenceOfNatNat, preimage_rev_Ico, finsetImage_addNat_Ici, finsetImage_castSucc_Ioo, image_succ_Iic, range_natAdd_eq_Ici, preimage_castSucc_Iic_castSucc, map_castLEEmb_Iic, card_Ici, prod_Ico_succ, orderHom_injective_iff, CategoryTheory.ComposableArrows.twoδ₁Toδ₀_app_zero, finsetImage_natAdd_Icc, SimplexCategory.const_comp, map_addNatEmb_Ici, CategoryTheory.ComposableArrows.scMap_τ₁, strictAnti_vecEmpty, CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso_inv_app, finsetImage_val_Ioi, Matrix.det_vandermonde, orderPred_succ, prod_Ioo_castLE, attachFin_Ioo_eq_Ioi, image_natAdd_Icc, find_mono_of_le, preimage_rev_Ici, finsetImage_val_Ioo, preimage_succ_Ioi_succ, image_natAdd_Ico, map_natAddEmb_Ici, SSet.prodStdSimplex.orderHomOfSimplex_coe, strictMono_succAbove, AugmentedSimplexCategory.eqToHom_toOrderHom, sum_sum_eq_sum_triangle_add, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₃, CategoryTheory.ComposableArrows.threeδ₂Toδ₁_app_one, Matrix.det_projVandermonde, finsetImage_castAdd_Iio, preimage_castSucc_Ico_castSucc, CategoryTheory.ComposableArrows.threeδ₁Toδ₀_app_zero, preimage_val_Ioc_val, finsetImage_castSucc_Ioc, SSet.prodStdSimplex.objEquiv_apply_fst, SSet.stdSimplex.map_id, CategoryTheory.ComposableArrows.threeδ₃Toδ₂_app_one, CategoryTheory.ComposableArrows.whiskerLeft_obj, sum_Icc_castAdd, List.SortedGT.strictAnti, sum_Ico_castSucc, image_addNat_Ici, preimage_natAdd_Icc_natAdd, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom, preimage_succ_Icc_succ, preimage_succ_Iic_succ, image_natAdd_Ici, CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_two, castSuccOrderEmb_toEmbedding, sum_Iic_cast, orderPred_zero, Equiv.Perm.sign_eq_prod_prod_Ioi, map_addNatEmb_Ioi, Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod, CategoryTheory.ShortComplex.mapToComposableArrows_app_1, Tuple.monotone_proj, finsetImage_castAdd_Iic, finsetImage_succ_Iio, CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac_assoc, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_obj, Module.Basis.flag_mono, SimplexCategory.mkOfSucc_homToOrderHom_one, map_castAddEmb_Ici, map_finCongr_Ioo, natAddOrderEmb_toEmbedding, SimplexCategory.Hom.mk_toOrderHom_apply, finsetImage_castLE_Ico, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, monotone_vecEmpty, CategoryTheory.Localization.essSurj_mapComposableArrows_of_hasRightCalculusOfFractions, SSet.stdSimplex.face_eq_ofSimplex, preimage_addNat_Iic_addNat, prod_Ioo_castAdd, finsetImage_succ_Ico, image_natAdd_Ioo, SSet.prodStdSimplex.objEquiv_δ_apply, CategoryTheory.ComposableArrows.precomp_obj, Tuple.sort_eq_refl_iff_monotone, CategoryTheory.ComposableArrows.Precomp.map_zero_succ_succ, sum_Ioo_succ, strictMono_vecEmpty, CategoryTheory.ComposableArrows.threeδ₂Toδ₁_app_two, sum_Iic_castAdd, preimage_castAdd_Ici_castAdd, preimage_cast_Ici, image_castLE_Iio, attachFin_Icc, map_finCongr_Iic, SSet.prodStdSimplex.objEquiv_naturality, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, preimage_cast_Iic, map_revPerm_Ico, image_castSucc_Ioc, finsetImage_castAdd_Ico, extDeriv_apply_vectorField, HomologicalComplex.HomologySequence.instEpiMap'ComposableArrows₃OfNatNat, attachFin_Ico_eq_Ici, CategoryTheory.ComposableArrows.exact_iff_δ₀, card_Ico, finsetImage_cast_Ioi, SimplexCategory.toTop_map, image_castAdd_Ioo, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, Ioo_add_one_eq_Ioc, sum_Ioi_cast, map_castLEEmb_Ico, sum_Ico_succ, preimage_val_Ioi_val, isAddFreimanIso_Iic, preimage_succ_Ioc_succ, image_succ_Ico, finsetImage_cast_Iio, finsetImage_val_Iio, SimplexCategory.II.map'_map', Ico_add_one_eq_Icc, SimplexCategory.toTop₀_map, preimage_succ_Iio_succ, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₁, PartialOrder.mem_nerve_nonDegenerate_iff_injective, SSet.prodStdSimplex.objEquiv_apply_snd, CategoryTheory.ComposableArrows.twoδ₂Toδ₁_app_zero, finsetImage_cast_Icc, CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_map, SimplexCategory.congr_toOrderHom_apply, CategoryTheory.Triangulated.SpectralObject.triangle_obj₂, finsetImage_castAdd_Ici, image_castSucc_Icc, finsetImage_cast_Ici, CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer', sum_Ioo_castLE, preimage_natAdd_Ioo_natAdd, image_val_Ici, sum_Ioc_castAdd, prod_Ici_cast, addRothNumber_eq_rothNumberNat, CategoryTheory.ComposableArrows.map'_comp, CategoryTheory.ComposableArrows.IsComplex.zero_assoc, preimage_castLE_Ioo_castLE, preimage_castLE_Ioi_castLE, Equiv.Perm.sign_eq_prod_prod_Iio, map_revPerm_Ici, SSet.horn_obj, CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map, sum_Ioo_cast, CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map, prod_Ioc_castLE, image_val_Ioc, finsetImage_castSucc_Ico, finsetImage_addNat_Ioc, map_castLEEmb_Ioo, sum_Icc_cast, preimage_rev_Icc, image_succ_Ici, CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac_assoc, CategoryTheory.ComposableArrows.δ₀Functor_obj_map, SSet.stdSimplex.face_obj, SSet.stdSimplex.nonDegenerateEquiv_apply_apply, sum_Ici_cast, map_revPerm_Icc, sum_Iic_castLE, CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_one, image_succ_Ioc, preimage_castAdd_Ioo_castAdd, prod_Ioc_castSucc, SSet.Truncated.spine_map_vertex, SimplexCategory.id_toOrderHom, List.SortedGT.strictAnti_get, CochainComplex.mappingConeCompTriangle_mor₃_naturality, List.sortedGT_iff_strictAnti_get, prod_Ioo_cast, classifyingSpaceUniversalCover_map, finsetImage_rev_Iic, List.SortedLE.monotone_get, sum_Ioc_castLE, sum_Iio_castLE, preimage_val_Iic_val, preimage_castAdd_Ioi_castAdd, finsetImage_val_Ioc, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id, map_revPerm_Ioi, Iio_last_eq_map, map_addNatEmb_Ico, preimage_val_Ico_val, preimage_cast_Ioi, List.SortedLE.monotone, CategoryTheory.ComposableArrows.whiskerLeftFunctor_obj_obj, Matrix.IsHermitian.eigenvalues₀_antitone, CategoryTheory.ComposableArrows.opEquivalence_functor_map_app, List.sorted_gt_ofFn_iff, map_castLEEmb_Icc, AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, prod_Iio_castSucc, CategoryTheory.Functor.mapComposableArrowsObjMk₂Iso_hom_app, val_strictMono, preimage_addNat_Ioi_addNat, preimage_addNat_Iio_addNat, image_castAdd_Iic, CategoryTheory.ComposableArrows.sc'MapIso_hom, preimage_natAdd_Ioc_natAdd, SSet.stdSimplex.coe_edge_down_toOrderHom, map_valEmbedding_Ici, CategoryTheory.ComposableArrows.opEquivalence_inverse_obj, SimplexCategory.eqToHom_toOrderHom, HomotopyCategory.composableArrowsFunctor_obj, prod_Icc_castLE, preimage_castAdd_Iio_castAdd, map_succEmb_Ioi, CategoryTheory.ComposableArrows.scMapIso_inv, image_val_Iio, finsetImage_rev_Ioc, map_finCongr_Ici, preimage_succ_Ico_succ, LTSeries.strictMono, List.Sorted.get_mono, card_Icc, SSet.OneTruncation₂.nerveEquiv_symm_apply_map, CategoryTheory.ComposableArrows.mk₁_obj, image_castAdd_Ici, SSet.stdSimplex.isoNerve_hom_app_apply, predAbove_right_monotone, CategoryTheory.ComposableArrows.whiskerLeft_map, finsetImage_rev_Ioi, prod_Iic_castSucc, preimage_castLE_Ioc_castLE, PartialOrder.mem_range_nerve_σ_iff, finsetImage_succ_Iic, strictMono_addNat, preimage_rev_Ioi, antitone_vecCons, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, CategoryTheory.ComposableArrows.mapFunctorArrows_app, SimplexCategory.II.castSucc_mem_finset_iff, CategoryTheory.ShortComplex.mapToComposableArrows_comp, CategoryTheory.Functor.mapComposableArrowsObjMk₁Iso_hom_app, prod_Ioi_cast, preimage_succ_Ioo_succ, CategoryTheory.Functor.mapComposableArrows_obj_map, finsetImage_castAdd_Ioi, prod_Iio_castAdd, SimplexCategory.mono_iff_injective, finsetImage_natAdd_Ico, sum_Ico_cast, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id, castLEOrderEmb_toEmbedding, orderPred_apply, image_castSucc_Ici, finsetImage_val_Ico, prod_Ico_cast, CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_obj, CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_ω₁, map_succEmb_Ici, SimplexCategory.II.map'_eq_last_iff, find_congr, preimage_rev_Ioc, map_natAddEmb_Icc, prod_Ioi_succ, CategoryTheory.Triangulated.SpectralObject.triangle_mor₂, finsetImage_cast_Ioo, image_natAdd_Ioc, card_Iio, CategoryTheory.ShortComplex.mapToComposableArrows_app_2, CategoryTheory.ComposableArrows.naturality', finsetImage_val_Ici, preimage_natAdd_Ico_natAdd, SimplexCategory.rev_map_apply, strictMono_succ, image_castSucc_Ioi, cast_strictMono, strictMono_iff_lt_succ, CategoryTheory.instEpiMap'KernelCokernelCompSequenceOfNatNat, card_Ioo, map_valEmbedding_Icc, CategoryTheory.ComposableArrows.sc'Map_τ₁, map_castSuccEmb_Ici, image_castAdd_Icc, SimplexCategory.mkOfSucc_homToOrderHom_zero, attachFin_Ico, prod_Iic_cast, SimplexCategory.II.map'_succAboveOrderEmb, image_castAdd_Ioc, SimplexCategory.instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat, List.sortedLT_iff_strictMono_get, finsetImage_addNat_Ico, extDerivWithin_apply_vectorField, CategoryTheory.Limits.FormalCoproduct.cechFunctor_map_app, CategoryTheory.Triangulated.SpectralObject.Hom.comm_assoc, map_natAddEmb_Ico, CategoryTheory.ComposableArrows.mk₀_obj, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₂, Tuple.comp_sort_eq_comp_iff_monotone, CategoryTheory.ComposableArrows.twoδ₁Toδ₀_app_one, image_addNat_Icc, CategoryTheory.Triangulated.SpectralObject.id_hom, preimage_castLE_Iic_castLE, preimage_addNat_Icc_addNat, image_addNat_Ioi, SSet.stdSimplex.monotone_apply, List.SortedGE.antitone, CategoryTheory.ComposableArrows.mk₁_map, preimage_castLE_Icc_castLE, CategoryTheory.ComposableArrows.threeδ₁Toδ₀_app_two, castAddOrderEmb_toEmbedding, SimplexCategory.II.map'_eq_castSucc_iff, PartialOrder.mem_nerve_nonDegenerate_iff_strictMono, CategoryTheory.ComposableArrows.isComplex₂_iff, SSet.prodStdSimplex.objEquiv_map_apply, predAboveOrderHom_coe, List.sorted_le_ofFn_iff, image_succ_Ioi, CategoryTheory.ComposableArrows.δlastFunctor_obj_obj, CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id_assoc, CompositionSeries.strictMono, CategoryTheory.Limits.FormalCoproduct.cech_map, SSet.horn.edge₃_coe_down, orderSucc_last, map_castAddEmb_Ioc, List.sortedLT_finRange, SSet.stdSimplex.const_down_toOrderHom, finsetImage_succ_Ioo, CategoryTheory.ComposableArrows.scMapIso_hom, CategoryTheory.ComposableArrows.opEquivalence_functor_obj_obj, attachFin_Ioo, List.Sorted.get_strictMono, prod_Ioo_castSucc, map_revPerm_Ioo, CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_three, CategoryTheory.Triangulated.SpectralObject.distinguished', preimage_castAdd_Icc_castAdd, Algebra.discr_powerBasis_eq_prod, CategoryTheory.Triangulated.SpectralObject.triangle_mor₁, Tuple.eq_sort_iff, finsetImage_castSucc_Ioi, List.sortedGT_ofFn_iff, List.SortedLT.strictMono_get, CategoryTheory.ComposableArrows.whiskerLeftFunctor_map_app, map_valEmbedding_Ioi, finsetImage_natAdd_Ioi, CategoryTheory.ComposableArrows.scMap_τ₃, CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_zero, CategoryTheory.ComposableArrows.δlastFunctor_map_app, SimplexCategoryGenRel.simplicialEvalσ_of_isAdmissible, finsetImage_val_Icc, image_val_Ioi, map_castLEEmb_Iio, preimage_cast_Iio, image_castAdd_Ioi, orderSucc_apply, succAboveOrderEmb_toEmbedding, HomotopyCategory.composableArrowsFunctor_map, SimplexCategory.II.monotone_map', CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ, prod_Ico_castSucc, strictMono_castSucc, CategoryTheory.ComposableArrows.sc'Map_τ₃, CategoryTheory.nerve.δ_obj, map_succEmb_Ioo, preimage_castSucc_Iio_castSucc, map_valEmbedding_Ioo, sum_Iio_castAdd, preimage_rev_Iio, orderPred_eq, map_castSuccEmb_Icc, SSet.spine_map_vertex, sum_Ioo_castAdd, image_castSucc_Ico, sum_Iio_cast, preimage_addNat_Ici_addNat, Iio_castSucc, map_castAddEmb_Iio, image_castSucc_Ioo, Ioc_sub_one_eq_Icc, Iio_add_one_eq_Iic, sum_Iio_castSucc, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac_assoc, card_Iic, prod_Icc_succ, image_castLE_Ico, SimplexCategory.II.map'_predAbove, preimage_natAdd_Iic_natAdd, SimplexCategory.II.mem_finset_iff, image_castLE_Iic, CategoryTheory.ComposableArrows.instIsIsoOfNatNatTwoδ₁Toδ₀, finsetImage_castSucc_Iic, attachFin_Iio, range_castAdd, CategoryTheory.ShortComplex.toComposableArrows_map, sort_univ, finsetImage_castSucc_Icc, sum_Icc_succ, map_natAddEmb_Ioi, map_valEmbedding_Ico, map_castSuccEmb_Iio, CategoryTheory.ComposableArrows.threeδ₃Toδ₂_app_two, SSet.stdSimplex.objEquiv_toOrderHom_apply, map_revPerm_Iio, addRothNumber_le_rothNumberNat, SimplexCategory.const_apply, AugmentedSimplexCategory.inl'_eval, CategoryTheory.ComposableArrows.isoMk₀_inv_app, CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_two, Icc_sub_one_eq_Ico, map_succEmb_Ico, prod_Iic_castLE, CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_one, preimage_val_Icc_val, CategoryTheory.Triangulated.SpectralObject.comp_hom, finsetImage_succ_Icc, preimage_rev_Iic, preimage_rev_Ioo, CategoryTheory.ComposableArrows.scMap_τ₂, prod_Ioc_castAdd, finsetImage_rev_Iio, CategoryTheory.ComposableArrows.isIso_iff₀, CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ', finsetImage_addNat_Icc, List.sorted_lt_ofFn_iff, map_castSuccEmb_Iic, map_finCongr_Ioi, sum_Icc_castLE, map_addNatEmb_Ioc, map_succEmb_Ioc, CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_obj, preimage_castSucc_Ici_castSucc, finsetImage_rev_Icc, HomologicalComplex.HomologySequence.instMonoMap'ComposableArrows₃OfNatNat, image_natAdd_Ioi, Tuple.eq_sort_iff', SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, Iic_sub_one_eq_Iio, Ici_add_one_eq_Ioi, SSet.stdSimplex.objMk_apply, CategoryTheory.ComposableArrows.twoδ₂Toδ₁_app_one, prod_Ioi_zero, sum_Ioc_succ, CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_one, image_castLE_Ioc, HomotopyCategory.spectralObjectMappingCone_ω₁, sum_Ico_castAdd, CategoryTheory.ComposableArrows.opEquivalence_inverse_map, prod_Icc_castSucc, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac, SimplexCategory.toType_apply, sum_Ioc_cast, List.SortedLT.strictMono, preimage_addNat_Ioo_addNat, CategoryTheory.Functor.mapComposableArrows_obj_obj, image_castAdd_Ico, prod_Ici_succ, CategoryTheory.Arrow.cechNerve_map, strictMono_castAdd, CategoryTheory.ShortComplex.toComposableArrows_obj, SimplexCategory.concreteCategoryHom_id, CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer', prod_Iio_cast, preimage_castSucc_Icc_castSucc, prod_Ico_castLE, sum_Iic_castSucc, prod_Icc_castAdd, List.sorted_ge_ofFn_iff, CategoryTheory.ComposableArrows.δ₀Functor_obj_obj, castSuccFunctor_obj, preimage_castSucc_Ioo_castSucc, image_succ_Icc, Ioo_sub_one_eq_Ico, preimage_castLE_Ici_castLE, CategoryTheory.Arrow.cechConerve_map, CategoryTheory.ComposableArrows.map'_self, CategoryTheory.ComposableArrows.Exact.isIso_cokerToKer', SSet.OneTruncation₂.nerveEquiv_symm_apply_obj, range_natAdd_eq_Ioi, antitone_iff_succ_le, preimage_castAdd_Ioc_castAdd, preimage_natAdd_Ici_natAdd, finsetImage_val_Iic, finsetImage_succ_Ici, finsetImage_castLE_Iic, SSet.OneTruncation₂.ofNerve₂.natIso_inv_app_obj_map, strictMono_vecCons, SimplexCategory.comp_toOrderHom, preimage_castAdd_Iic_castAdd, OrderedFinpartition.parts_strictMono, Algebra.discr_powerBasis_eq_prod'', SimplexCategory.II.map'_id, image_val_Ico, preimage_castLE_Ico_castLE, preimage_cast_Ioo, CategoryTheory.ComposableArrows.threeδ₁Toδ₀_app_one, CategoryTheory.nerve.ext_of_isThin_iff, CategoryTheory.ComposableArrows.threeδ₃Toδ₂_app_zero, Ioc_sub_one_eq_Ioo, List.sortedGE_iff_antitone_get, CategoryTheory.ComposableArrows.fourδ₂Toδ₁_app_two, finsetImage_addNat_Ioo, List.SortedGE.antitone_get, castSuccFunctor_map, card_Ioc, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₂, preimage_castSucc_Ioc_castSucc, rev_strictAnti, finsetImage_castSucc_Ici, prod_Iio_castLE, CategoryTheory.Triangulated.SpectralObject.triangle_obj₃, finsetImage_rev_Ico, preimage_val_Ioo_val, CategoryTheory.ComposableArrows.mk₀_map, SSet.horn.primitiveEdge_coe_down, Algebra.discr_powerBasis_eq_prod', CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_two, CategoryTheory.Triangulated.SpectralObject.comp_hom_assoc, map_castSuccEmb_Ioi, finsetImage_castSucc_Iio, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_incl_app, map_succEmb_Icc, HomologicalComplex.HomologySequence.composableArrows₃Functor_map, OrderedFinpartition.emb_strictMono, sum_Icc_castSucc, CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₂, Ioi_sub_one_eq_Ici, finsetImage_cast_Iic, map_finCongr_Iio, orderSucc_castSucc, strictMono_castLE, CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_three, finsetImage_castAdd_Icc, map_castSuccEmb_Ico, map_addNatEmb_Icc, map_castSuccEmb_Ioo, preimage_castSucc_Ioi_castSucc, finsetImage_castLE_Ioc, CategoryTheory.ComposableArrows.Precomp.map_comp, image_succ_Iio, prod_Ioc_succ, CategoryTheory.Triangulated.SpectralObject.triangle_obj₁, finsetImage_natAdd_Ioo, CategoryTheory.ComposableArrows.δ₀Functor_map_app, RootPairing.Base.exists_eq_sum_and_forall_sum_mem_of_isPos, List.sortedLE_ofFn_iff, preimage_cast_Ico, rev_anti, HomologicalComplex.HomologySequence.composableArrows₃Functor_obj, CategoryTheory.ComposableArrows.sc'Map_τ₂, CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_exists, CategoryTheory.ComposableArrows.isoMk₀_hom_app, preimage_addNat_Ico_addNat, CategoryTheory.ComposableArrows.functorArrows_map, CategoryTheory.nerveMap_app, image_addNat_Ioc, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac_assoc, CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_one, List.sortedLT_ofFn_iff, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₁, prod_Icc_cast, map_castAddEmb_Iic, finsetImage_cast_Ioc, map_valEmbedding_Iio, strictAnti_iff_succ_lt, sum_Ico_castLE, prod_Iic_castAdd, strictAnti_vecCons, Ioi_zero_eq_map, map_finCongr_Ioc, CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map, CategoryTheory.TransfiniteCompositionOfShape.ofComposableArrows_isColimit, AugmentedSimplexCategory.inr'_eval, map_natAddEmb_Ioo, image_succ_Ioo, sum_Ioi_zero, Icc_add_one_eq_Ioc, Equiv.Perm.monotone_iff, image_castSucc_Iic, map_addNatEmb_Ioo, CategoryTheory.ComposableArrows.naturality'_assoc, finsetImage_cast_Ico, preimage_addNat_Ioc_addNat, CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₃, CategoryTheory.ComposableArrows.instIsIsoOfNatNatTwoδ₂Toδ₁, finsetImage_castAdd_Ioo, image_addNat_Ico, finsetImage_natAdd_Ici, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app, finsetImage_rev_Ioo, sum_Ioc_castSucc, CategoryTheory.ComposableArrows.functorArrows_obj, orderSucc_eq, succFunctor_obj, finsetImage_succ_Ioc, CategoryTheory.Limits.FormalCoproduct.cech_obj, preimage_castLE_Iio_castLE, map_castAddEmb_Icc, List.sortedLE_iff_monotone_get, CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_zero, preimage_cast_Icc, SSet.stdSimplex.objEquiv_symm_apply, CategoryTheory.ComposableArrows.Mk₁.map_comp, CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac, map_castAddEmb_Ioo, Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod, preimage_succ_Ici_succ, finsetImage_castAdd_Ioc, DivisorChain.exists_chain_of_prime_pow, CategoryTheory.ShortComplex.mapToComposableArrows_id, CategoryTheory.ComposableArrows.precomp_map, CategoryTheory.ComposableArrows.fourδ₁Toδ₀_app_three, sum_Ioo_castSucc, CategoryTheory.ComposableArrows.IsComplex.zero, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac, SSet.stdSimplex.nonDegenerateEquiv_symm_apply_coe, antitone_vecEmpty, map_natAddEmb_Ioc, monotone_vecCons, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₁, Module.Basis.flag_strictMono, map_castSuccEmb_Ioc, prod_prod_eq_prod_triangle_mul, CategoryTheory.ComposableArrows.homMk₀_app, SimplexCategory.epi_iff_surjective, map_revPerm_Iic, sum_Ioi_succ, CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_three, List.sortedGE_ofFn_iff, image_val_Icc, map_finCongr_Icc, succFunctor_map, map_succEmb_Iic, finsetImage_rev_Ici, CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_zero, preimage_cast_Ioc, prod_Ioc_cast, preimage_val_Iio_val, CategoryTheory.Functor.instIsWellOrderContinuousFin, map_finCongr_Ico, finsetImage_succ_Ioi, CategoryTheory.Localization.essSurj_mapComposableArrows, CategoryTheory.ComposableArrows.isIso_iff₁, CategoryTheory.nerve.δ₂_two, sum_Ici_succ, map_valEmbedding_Iic, LinearMap.IsSymmetric.eigenvalues_antitone, CategoryTheory.ComposableArrows.IsComplex.zero', image_castAdd_Iio, image_castSucc_Iio, Tuple.monotone_sort, map_valEmbedding_Ioc, monotone_iff_le_succ, prod_Ioo_succ, attachFin_Ioc, LTSeries.monotone, map_castAddEmb_Ioi, SSet.stdSimplex.isoNerve_inv_app_apply, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac_assoc, CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₃, strictMono_natAdd, CategoryTheory.ComposableArrows.δlastFunctor_obj_map, finsetImage_castLE_Icc, image_val_Ioo, prod_Ico_castAdd, CategoryTheory.ComposableArrows.Precomp.map_one_one, CategoryTheory.Functor.mapComposableArrows_map_app
natAddOrderEmb 📖	CompOp	2 math math: natAddOrderEmb_toEmbedding, natAddOrderEmb_apply
orderIsoSubtype 📖	CompOp	2 math math: orderIsoSubtype_apply, orderIsoSubtype_symm_apply
predAboveOrderHom 📖	CompOp	1 math math: predAboveOrderHom_coe
revOrderIso 📖	CompOp	11 math math: CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, revOrderIso_apply, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map, CategoryTheory.ComposableArrows.opEquivalence_functor_map_app, CategoryTheory.ComposableArrows.opEquivalence_inverse_obj, revOrderIso_toEquiv, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, revOrderIso_symm_apply, CategoryTheory.ComposableArrows.opEquivalence_inverse_map, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app
succAboveOrderEmb 📖	CompOp	5 math math: SimplexCategory.II.map'_succAboveOrderEmb, Finset.orderEmbOfFin_compl_singleton_eq_succAboveOrderEmb, succAboveOrderEmb_toEmbedding, Finset.orderEmbOfFin_compl_singleton, succAboveOrderEmb_apply
succOrderEmb 📖	CompOp	2 math math: succOrderEmb_toEmbedding, coe_succOrderEmb
valOrderEmb 📖	CompOp	2 math math: valOrderEmb_apply, OrderEmbedding.default_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addNatOrderEmb_apply 📖	mathematical	—	DFunLike.coe RelEmbedding RelEmbedding.instFunLike addNatOrderEmb	—	—
addNatOrderEmb_toEmbedding 📖	mathematical	—	RelEmbedding.toEmbedding addNatOrderEmb Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder instPartialOrder instAntisymmLe instReflLe StrictMono.le_iff_le strictMono_addNat	—	—
addNat_inj 📖	—	—	—	—	StrictMono.injective strictMono_addNat
addNat_le_addNat_iff 📖	—	—	—	—	StrictMono.le_iff_le strictMono_addNat
addNat_lt_addNat_iff 📖	—	—	—	—	StrictMono.lt_iff_lt strictMono_addNat
antitone_iff_succ_le 📖	mathematical	—	Antitone PartialOrder.toPreorder instPartialOrder Preorder.toLE	—	antitone_iff_forall_lt liftFun_iff_succ instIsTransGe
bot_eq_zero 📖	mathematical	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra instHeytingAlgebra HeytingAlgebra.toOrderBot	—	—
castAddOrderEmb_apply 📖	mathematical	—	DFunLike.coe RelEmbedding RelEmbedding.instFunLike castAddOrderEmb	—	—
castAddOrderEmb_toEmbedding 📖	mathematical	—	RelEmbedding.toEmbedding castAddOrderEmb Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder instPartialOrder instAntisymmLe instReflLe StrictMono.le_iff_le strictMono_castAdd	—	—
castLEOrderEmb_apply 📖	mathematical	—	DFunLike.coe RelEmbedding RelEmbedding.instFunLike castLEOrderEmb	—	—
castLEOrderEmb_toEmbedding 📖	mathematical	—	RelEmbedding.toEmbedding castLEOrderEmb Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder instPartialOrder instAntisymmLe instReflLe StrictMono.le_iff_le strictMono_castLE	—	—
castLE_le_castLE_iff 📖	—	—	—	—	—
castLE_lt_castLE_iff 📖	—	—	—	—	—
castOrderIso_apply 📖	mathematical	—	DFunLike.coe RelIso RelIso.instFunLike castOrderIso	—	—
castOrderIso_refl 📖	mathematical	—	castOrderIso OrderIso.refl	—	OrderIso.ext
castOrderIso_symm_apply 📖	mathematical	—	DFunLike.coe RelIso RelIso.instFunLike RelIso.symm castOrderIso	—	—
castOrderIso_toEquiv 📖	mathematical	—	RelIso.toEquiv castOrderIso Equiv.cast	—	—
castSuccOrderEmb_apply 📖	mathematical	—	DFunLike.coe RelEmbedding RelEmbedding.instFunLike castSuccOrderEmb	—	—
castSuccOrderEmb_toEmbedding 📖	mathematical	—	RelEmbedding.toEmbedding castSuccOrderEmb Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder instPartialOrder instAntisymmLe instReflLe StrictMono.le_iff_le strictMono_castSucc	—	—
cast_strictMono 📖	mathematical	—	StrictMono PartialOrder.toPreorder instPartialOrder	—	—
cast_top 📖	mathematical	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra instCoheytingAlgebra CoheytingAlgebra.toOrderTop	—	—
coe_max 📖	mathematical	—	instMax_mathlib	—	—
coe_min 📖	mathematical	—	instMin_mathlib	—	—
coe_orderIso_apply 📖	mathematical	—	DFunLike.coe OrderIso instFunLikeOrderIso	—	Nat.strong_induction_on le_antisymm forall_lt_iff_le OrderIso.lt_symm_apply OrderIso.apply_symm_apply LT.lt.trans OrderIso.lt_iff_lt
coe_succOrderEmb 📖	mathematical	—	DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding succOrderEmb	—	—
compare_eq_compare_val 📖	—	—	—	—	—
monotone_castPred_comp 📖	mathematical	Monotone PartialOrder.toPreorder instPartialOrder	castPred	—	castPred_le_castPred_iff
monotone_iff_le_succ 📖	mathematical	—	Monotone PartialOrder.toPreorder instPartialOrder Preorder.toLE	—	monotone_iff_forall_lt liftFun_iff_succ instIsTransLe
monotone_pred_comp 📖	—	Monotone PartialOrder.toPreorder instPartialOrder	—	—	—
natAddOrderEmb_apply 📖	mathematical	—	DFunLike.coe RelEmbedding RelEmbedding.instFunLike natAddOrderEmb	—	—
natAddOrderEmb_toEmbedding 📖	mathematical	—	RelEmbedding.toEmbedding natAddOrderEmb Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder instPartialOrder instAntisymmLe instReflLe StrictMono.le_iff_le strictMono_natAdd	—	—
natAdd_inj 📖	—	—	—	—	StrictMono.injective strictMono_natAdd
natAdd_injective 📖	—	—	—	—	StrictMono.injective strictMono_natAdd
natAdd_le_natAdd_iff 📖	—	—	—	—	StrictMono.le_iff_le strictMono_natAdd
natAdd_lt_natAdd_iff 📖	—	—	—	—	StrictMono.lt_iff_lt strictMono_natAdd
orderHom_injective_iff 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder instPartialOrder OrderHom.instFunLike	—	StrictMono.injective strictMono_iff_lt_succ lt_of_le_of_ne OrderHom.monotone castSucc_le_succ
orderIsoSubtype_apply 📖	mathematical	—	DFunLike.coe RelIso RelIso.instFunLike orderIsoSubtype	—	—
orderIsoSubtype_symm_apply 📖	mathematical	—	DFunLike.coe RelIso RelIso.instFunLike RelIso.symm orderIsoSubtype	—	—
predAboveOrderHom_coe 📖	mathematical	—	DFunLike.coe OrderHom PartialOrder.toPreorder instPartialOrder OrderHom.instFunLike predAboveOrderHom predAbove	—	—
predAbove_le_predAbove 📖	mathematical	—	predAbove	—	LE.le.trans predAbove_right_monotone predAbove_left_monotone
predAbove_left_inj 📖	mathematical	—	predAbove	—	predAbove_left_injective
predAbove_left_injective 📖	mathematical	—	predAbove	—	size_positive LT.lt.ne castSucc_castPred predAbove_of_le_castSucc predAbove_succ_self LE.le.lt_or_eq
predAbove_left_monotone 📖	mathematical	—	Monotone PartialOrder.toPreorder instPartialOrder predAbove	—	le_refl LT.lt.trans_le le_of_not_gt LT.lt.not_ge
predAbove_right_monotone 📖	mathematical	—	Monotone PartialOrder.toPreorder instPartialOrder predAbove	—	LE.le.trans_lt not_lt
revOrderIso_apply 📖	mathematical	—	DFunLike.coe RelIso OrderDual OrderDual.instLE RelIso.instFunLike revOrderIso Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual	—	—
revOrderIso_symm_apply 📖	mathematical	—	DFunLike.coe OrderIso OrderDual OrderDual.instLE instFunLikeOrderIso OrderIso.symm revOrderIso Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual	—	—
revOrderIso_toEquiv 📖	mathematical	—	RelIso.toEquiv OrderDual OrderDual.instLE revOrderIso Equiv.trans OrderDual.ofDual revPerm	—	—
rev_anti 📖	mathematical	—	Antitone PartialOrder.toPreorder instPartialOrder	—	StrictAnti.antitone rev_strictAnti
rev_bot 📖	mathematical	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra instHeytingAlgebra HeytingAlgebra.toOrderBot Top.top OrderTop.toTop GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra instCoheytingAlgebra CoheytingAlgebra.toOrderTop	—	—
rev_last_eq_bot 📖	mathematical	—	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra instHeytingAlgebra HeytingAlgebra.toOrderBot	—	bot_eq_zero
rev_strictAnti 📖	mathematical	—	StrictAnti PartialOrder.toPreorder instPartialOrder	—	—
rev_top 📖	mathematical	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra instCoheytingAlgebra CoheytingAlgebra.toOrderTop Bot.bot OrderBot.toBot GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra instHeytingAlgebra HeytingAlgebra.toOrderBot	—	—
rev_zero_eq_top 📖	mathematical	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra instCoheytingAlgebra CoheytingAlgebra.toOrderTop	—	—
strictAnti_iff_succ_lt 📖	mathematical	—	StrictAnti PartialOrder.toPreorder instPartialOrder Preorder.toLT	—	liftFun_iff_succ instIsTransGt
strictMono_addNat 📖	mathematical	—	StrictMono PartialOrder.toPreorder instPartialOrder	—	—
strictMono_castAdd 📖	mathematical	—	StrictMono PartialOrder.toPreorder instPartialOrder	—	strictMono_castLE
strictMono_castLE 📖	mathematical	—	StrictMono PartialOrder.toPreorder instPartialOrder	—	—
strictMono_castPred_comp 📖	mathematical	StrictMono PartialOrder.toPreorder instPartialOrder	castPred	—	castPred_lt_castPred_iff
strictMono_castSucc 📖	mathematical	—	StrictMono PartialOrder.toPreorder instPartialOrder	—	strictMono_castAdd
strictMono_iff_lt_succ 📖	mathematical	—	StrictMono PartialOrder.toPreorder instPartialOrder Preorder.toLT	—	liftFun_iff_succ instIsTransLt
strictMono_natAdd 📖	mathematical	—	StrictMono PartialOrder.toPreorder instPartialOrder	—	—
strictMono_pred_comp 📖	—	StrictMono PartialOrder.toPreorder instPartialOrder	—	—	—
strictMono_succ 📖	mathematical	—	StrictMono PartialOrder.toPreorder instPartialOrder	—	—
strictMono_succAbove 📖	mathematical	—	StrictMono PartialOrder.toPreorder instPartialOrder succAbove	—	StrictMono.ite strictMono_castSucc strictMono_succ LT.lt.trans LT.lt.le
succAboveOrderEmb_apply 📖	mathematical	—	DFunLike.coe RelEmbedding RelEmbedding.instFunLike succAboveOrderEmb succAbove	—	—
succAboveOrderEmb_toEmbedding 📖	mathematical	—	RelEmbedding.toEmbedding succAboveOrderEmb succAbove Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrder instPartialOrder instAntisymmLe instReflLe StrictMono.le_iff_le strictMono_succAbove	—	—
succAbove_inj 📖	mathematical	—	succAbove	—	StrictMono.injective strictMono_succAbove
succAbove_le_succAbove_iff 📖	mathematical	—	succAbove	—	StrictMono.le_iff_le strictMono_succAbove
succAbove_lt_succAbove_iff 📖	mathematical	—	succAbove	—	StrictMono.lt_iff_lt strictMono_succAbove
succOrderEmb_toEmbedding 📖	mathematical	—	RelEmbedding.toEmbedding succOrderEmb succEmb	—	—
succ_top 📖	mathematical	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra instCoheytingAlgebra CoheytingAlgebra.toOrderTop	—	rev_zero_eq_top castSucc_zero'
symm_castOrderIso 📖	mathematical	—	OrderIso.symm castOrderIso	—	—
top_eq_last 📖	mathematical	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra instCoheytingAlgebra CoheytingAlgebra.toOrderTop	—	—
top_eq_zero 📖	mathematical	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra instCoheytingAlgebra CoheytingAlgebra.toOrderTop	—	zero_eq_top
valOrderEmb_apply 📖	mathematical	—	DFunLike.coe RelEmbedding RelEmbedding.instFunLike valOrderEmb	—	—
val_strictMono 📖	mathematical	—	StrictMono PartialOrder.toPreorder instPartialOrder Nat.instPreorder	—	—
val_top 📖	mathematical	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra instCoheytingAlgebra CoheytingAlgebra.toOrderTop	—	—
zero_eq_top 📖	mathematical	—	Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra instCoheytingAlgebra CoheytingAlgebra.toOrderTop	—	bot_eq_zero subsingleton_iff_bot_eq_top

Fin.Lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isWellOrder 📖	mathematical	—	IsWellOrder	—	OrderEmbedding.isWellOrder isWellOrder_lt instWellFoundedLTNat

Fin.OrderEmbedding

Definitions

Name	Category	Theorems
instInhabitedOrderEmbeddingNat 📖	CompOp	1 math math: default_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
default_def 📖	mathematical	—	OrderEmbedding instInhabitedOrderEmbeddingNat Fin.valOrderEmb	—	—

---

← Back to Index