| Metric | Count |
|---|
DefinitionsinstLocallyFiniteOrder, instLocallyFiniteOrderBot, instLocallyFiniteOrderTop | 3 |
TheoremsIcc_add_one_eq_Ioc, Icc_sub_one_eq_Ico, Ici_add_one_eq_Ioi, Ico_add_one_eq_Icc, Ico_add_one_eq_Ioo, Iic_sub_one_eq_Iio, Iio_add_one_eq_Iic, Ioc_sub_one_eq_Icc, Ioc_sub_one_eq_Ioo, Ioi_sub_one_eq_Ici, Ioo_add_one_eq_Ioc, Ioo_sub_one_eq_Ico, attachFin_Icc, attachFin_Ico, attachFin_Ico_eq_Ici, attachFin_Iic, attachFin_Iio, attachFin_Ioc, attachFin_Ioo, attachFin_Ioo_eq_Ioi, attachFin_uIcc, card_Icc, card_Ici, card_Ico, card_Iic, card_Iio, card_Ioc, card_Ioi, card_Ioo, card_uIcc, finsetImage_addNat_Icc, finsetImage_addNat_Ici, finsetImage_addNat_Ico, finsetImage_addNat_Ioc, finsetImage_addNat_Ioi, finsetImage_addNat_Ioo, finsetImage_addNat_uIcc, finsetImage_castAdd_Icc, finsetImage_castAdd_Ici, finsetImage_castAdd_Ico, finsetImage_castAdd_Iic, finsetImage_castAdd_Iio, finsetImage_castAdd_Ioc, finsetImage_castAdd_Ioi, finsetImage_castAdd_Ioo, finsetImage_castAdd_uIcc, finsetImage_castLE_Icc, finsetImage_castLE_Ico, finsetImage_castLE_Iic, finsetImage_castLE_Iio, finsetImage_castLE_Ioc, finsetImage_castLE_Ioo, finsetImage_castLE_uIcc, finsetImage_castSucc_Icc, finsetImage_castSucc_Ici, finsetImage_castSucc_Ico, finsetImage_castSucc_Iic, finsetImage_castSucc_Iio, finsetImage_castSucc_Ioc, finsetImage_castSucc_Ioi, finsetImage_castSucc_Ioo, finsetImage_castSucc_uIcc, finsetImage_cast_Icc, finsetImage_cast_Ici, finsetImage_cast_Ico, finsetImage_cast_Iic, finsetImage_cast_Iio, finsetImage_cast_Ioc, finsetImage_cast_Ioi, finsetImage_cast_Ioo, finsetImage_cast_uIcc, finsetImage_natAdd_Icc, finsetImage_natAdd_Ici, finsetImage_natAdd_Ico, finsetImage_natAdd_Ioc, finsetImage_natAdd_Ioi, finsetImage_natAdd_Ioo, finsetImage_natAdd_uIcc, finsetImage_rev_Icc, finsetImage_rev_Ici, finsetImage_rev_Ico, finsetImage_rev_Iic, finsetImage_rev_Iio, finsetImage_rev_Ioc, finsetImage_rev_Ioi, finsetImage_rev_Ioo, finsetImage_rev_uIcc, finsetImage_succ_Icc, finsetImage_succ_Ici, finsetImage_succ_Ico, finsetImage_succ_Iic, finsetImage_succ_Iio, finsetImage_succ_Ioc, finsetImage_succ_Ioi, finsetImage_succ_Ioo, finsetImage_succ_uIcc, finsetImage_val_Icc, finsetImage_val_Ici, finsetImage_val_Ico, finsetImage_val_Iic, finsetImage_val_Iio, finsetImage_val_Ioc, finsetImage_val_Ioi, finsetImage_val_Ioo, finsetImage_val_uIcc, map_addNatEmb_Icc, map_addNatEmb_Ici, map_addNatEmb_Ico, map_addNatEmb_Ioc, map_addNatEmb_Ioi, map_addNatEmb_Ioo, map_addNatEmb_uIcc, map_castAddEmb_Icc, map_castAddEmb_Ici, map_castAddEmb_Ico, map_castAddEmb_Iic, map_castAddEmb_Iio, map_castAddEmb_Ioc, map_castAddEmb_Ioi, map_castAddEmb_Ioo, map_castAddEmb_uIcc, map_castLEEmb_Icc, map_castLEEmb_Ico, map_castLEEmb_Iic, map_castLEEmb_Iio, map_castLEEmb_Ioc, map_castLEEmb_Ioo, map_castLEEmb_uIcc, map_castSuccEmb_Icc, map_castSuccEmb_Ici, map_castSuccEmb_Ico, map_castSuccEmb_Iic, map_castSuccEmb_Iio, map_castSuccEmb_Ioc, map_castSuccEmb_Ioi, map_castSuccEmb_Ioo, map_castSuccEmb_uIcc, map_finCongr_Icc, map_finCongr_Ici, map_finCongr_Ico, map_finCongr_Iic, map_finCongr_Iio, map_finCongr_Ioc, map_finCongr_Ioi, map_finCongr_Ioo, map_finCongr_uIcc, map_natAddEmb_Icc, map_natAddEmb_Ici, map_natAddEmb_Ico, map_natAddEmb_Ioc, map_natAddEmb_Ioi, map_natAddEmb_Ioo, map_natAddEmb_uIcc, map_revPerm_Icc, map_revPerm_Ici, map_revPerm_Ico, map_revPerm_Iic, map_revPerm_Iio, map_revPerm_Ioc, map_revPerm_Ioi, map_revPerm_Ioo, map_revPerm_uIcc, map_succEmb_Icc, map_succEmb_Ici, map_succEmb_Ico, map_succEmb_Iic, map_succEmb_Iio, map_succEmb_Ioc, map_succEmb_Ioi, map_succEmb_Ioo, map_succEmb_uIcc, map_valEmbedding_Icc, map_valEmbedding_Ici, map_valEmbedding_Ico, map_valEmbedding_Iic, map_valEmbedding_Iio, map_valEmbedding_Ioc, map_valEmbedding_Ioi, map_valEmbedding_Ioo, map_valEmbedding_uIcc | 180 |
| Total | 183 |
| Name | Category | Theorems |
|---|
instLocallyFiniteOrder 📖 | CompOp | 170 mathmath: map_succEmb_Iio, finsetImage_natAdd_Ioc, prod_uIcc_cast, Ico_add_one_eq_Ioo, map_castLEEmb_Ioc, finsetImage_castLE_Ioo, map_revPerm_Ioc, map_castAddEmb_Ico, finsetImage_castAdd_uIcc, finsetImage_castSucc_Ioo, finsetImage_castSucc_uIcc, prod_Ico_succ, finsetImage_natAdd_Icc, prod_Ioo_castLE, finsetImage_val_Ioo, map_castLEEmb_uIcc, finsetImage_castSucc_Ioc, sum_Icc_castAdd, sum_Ico_castSucc, map_valEmbedding_uIcc, map_succEmb_uIcc, finsetImage_succ_Iio, card_uIcc, map_castAddEmb_Ici, map_finCongr_Ioo, finsetImage_castLE_Ico, prod_Ioo_castAdd, finsetImage_succ_Ico, sum_Ioo_succ, map_natAddEmb_uIcc, attachFin_Icc, map_revPerm_Ico, finsetImage_castAdd_Ico, card_Ico, Ioo_add_one_eq_Ioc, map_castLEEmb_Ico, sum_Ico_succ, Ico_add_one_eq_Icc, finsetImage_cast_Icc, finsetImage_castAdd_Ici, sum_Ioo_castLE, sum_Ioc_castAdd, sum_Ioo_cast, prod_Ioc_castLE, finsetImage_castSucc_Ico, finsetImage_addNat_Ioc, map_castLEEmb_Ioo, sum_Icc_cast, prod_uIcc_castLE, map_revPerm_Icc, prod_Ioc_castSucc, finsetImage_succ_uIcc, prod_Ioo_cast, map_finCongr_uIcc, sum_Ioc_castLE, finsetImage_val_Ioc, map_addNatEmb_Ico, map_castLEEmb_Icc, prod_Icc_castLE, finsetImage_castLE_uIcc, finsetImage_rev_Ioc, card_Icc, finsetImage_succ_Iic, finsetImage_rev_uIcc, prod_uIcc_castSucc, finsetImage_castAdd_Ioi, finsetImage_natAdd_Ico, sum_Ico_cast, finsetImage_val_Ico, attachFin_uIcc, prod_Ico_cast, map_natAddEmb_Icc, finsetImage_cast_Ioo, card_Ioo, map_valEmbedding_Icc, map_castSuccEmb_Ici, attachFin_Ico, finsetImage_addNat_Ico, map_natAddEmb_Ico, map_castAddEmb_Ioc, finsetImage_succ_Ioo, attachFin_Ioo, prod_Ioo_castSucc, map_revPerm_Ioo, map_revPerm_uIcc, finsetImage_castSucc_Ioi, finsetImage_val_Icc, map_addNatEmb_uIcc, prod_Ico_castSucc, map_succEmb_Ioo, map_valEmbedding_Ioo, sum_uIcc_castAdd, map_castSuccEmb_Icc, sum_Ioo_castAdd, Ioc_sub_one_eq_Icc, map_castAddEmb_uIcc, prod_Icc_succ, finsetImage_castSucc_Icc, sum_Icc_succ, map_valEmbedding_Ico, map_castSuccEmb_uIcc, Icc_sub_one_eq_Ico, map_succEmb_Ico, finsetImage_succ_Icc, prod_Ioc_castAdd, finsetImage_addNat_Icc, sum_Icc_castLE, map_addNatEmb_Ioc, map_succEmb_Ioc, finsetImage_rev_Icc, sum_uIcc_castSucc, sum_Ioc_succ, sum_Ico_castAdd, prod_Icc_castSucc, sum_Ioc_cast, prod_Ico_castLE, prod_Icc_castAdd, Ioo_sub_one_eq_Ico, sum_uIcc_castLE, finsetImage_natAdd_uIcc, prod_uIcc_succ, finsetImage_val_uIcc, Ioc_sub_one_eq_Ioo, finsetImage_addNat_Ioo, card_Ioc, prod_uIcc_castAdd, finsetImage_castSucc_Ici, finsetImage_rev_Ico, map_castSuccEmb_Ioi, map_succEmb_Icc, sum_Icc_castSucc, finsetImage_castAdd_Icc, map_castSuccEmb_Ico, map_addNatEmb_Icc, map_castSuccEmb_Ioo, finsetImage_castLE_Ioc, prod_Ioc_succ, finsetImage_natAdd_Ioo, prod_Icc_cast, finsetImage_cast_Ioc, sum_Ico_castLE, map_finCongr_Ioc, map_natAddEmb_Ioo, Icc_add_one_eq_Ioc, map_addNatEmb_Ioo, finsetImage_cast_Ico, finsetImage_castAdd_Ioo, finsetImage_rev_Ioo, sum_Ioc_castSucc, finsetImage_cast_uIcc, finsetImage_succ_Ioc, map_castAddEmb_Icc, map_castAddEmb_Ioo, finsetImage_castAdd_Ioc, sum_Ioo_castSucc, map_natAddEmb_Ioc, map_castSuccEmb_Ioc, sum_uIcc_cast, finsetImage_addNat_uIcc, map_finCongr_Icc, map_succEmb_Iic, prod_Ioc_cast, map_finCongr_Ico, map_valEmbedding_Ioc, prod_Ioo_succ, attachFin_Ioc, map_castAddEmb_Ioi, finsetImage_castLE_Icc, prod_Ico_castAdd, sum_uIcc_succ
|
instLocallyFiniteOrderBot 📖 | CompOp | 61 mathmath: finsetImage_castLE_Iio, map_succEmb_Iio, attachFin_Iic, map_castLEEmb_Iic, finsetImage_castAdd_Iio, sum_Iic_cast, finsetImage_castAdd_Iic, finsetImage_succ_Iio, sum_Iic_castAdd, map_finCongr_Iic, finsetImage_cast_Iio, finsetImage_val_Iio, addRothNumber_eq_rothNumberNat, Equiv.Perm.sign_eq_prod_prod_Iio, map_revPerm_Ici, sum_Iic_castLE, finsetImage_rev_Iic, sum_Iio_castLE, map_revPerm_Ioi, Iio_last_eq_map, prod_Iio_castSucc, finsetImage_rev_Ioi, prod_Iic_castSucc, finsetImage_succ_Iic, prod_Iio_castAdd, card_Iio, prod_Iic_cast, map_castLEEmb_Iio, sum_Iio_castAdd, sum_Iio_cast, Iio_castSucc, map_castAddEmb_Iio, Iio_add_one_eq_Iic, sum_Iio_castSucc, card_Iic, finsetImage_castSucc_Iic, attachFin_Iio, map_castSuccEmb_Iio, map_revPerm_Iio, addRothNumber_le_rothNumberNat, prod_Iic_castLE, finsetImage_rev_Iio, map_castSuccEmb_Iic, Iic_sub_one_eq_Iio, prod_Iio_cast, sum_Iic_castSucc, finsetImage_val_Iic, finsetImage_castLE_Iic, prod_Iio_castLE, finsetImage_castSucc_Iio, finsetImage_cast_Iic, map_finCongr_Iio, RootPairing.Base.exists_eq_sum_and_forall_sum_mem_of_isPos, map_castAddEmb_Iic, map_valEmbedding_Iio, prod_Iic_castAdd, Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod, map_revPerm_Iic, map_succEmb_Iic, finsetImage_rev_Ici, map_valEmbedding_Iic
|
instLocallyFiniteOrderTop 📖 | CompOp | 67 mathmath: card_Ioi, Ioi_succ, finsetImage_addNat_Ioi, finsetImage_addNat_Ici, card_Ici, map_addNatEmb_Ici, finsetImage_val_Ioi, Matrix.det_vandermonde, attachFin_Ioo_eq_Ioi, map_natAddEmb_Ici, sum_sum_eq_sum_triangle_add, Matrix.det_projVandermonde, Equiv.Perm.sign_eq_prod_prod_Ioi, map_addNatEmb_Ioi, Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod, map_castAddEmb_Ici, extDeriv_apply_vectorField, attachFin_Ico_eq_Ici, finsetImage_cast_Ioi, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, sum_Ioi_cast, finsetImage_castAdd_Ici, finsetImage_cast_Ici, prod_Ici_cast, map_revPerm_Ici, sum_Ici_cast, finsetImage_rev_Iic, map_revPerm_Ioi, AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, map_valEmbedding_Ici, map_succEmb_Ioi, map_finCongr_Ici, finsetImage_rev_Ioi, prod_Ioi_cast, finsetImage_castAdd_Ioi, map_succEmb_Ici, prod_Ioi_succ, finsetImage_val_Ici, map_castSuccEmb_Ici, extDerivWithin_apply_vectorField, Algebra.discr_powerBasis_eq_prod, finsetImage_castSucc_Ioi, map_valEmbedding_Ioi, finsetImage_natAdd_Ioi, map_natAddEmb_Ioi, map_revPerm_Iio, finsetImage_rev_Iio, map_finCongr_Ioi, Ici_add_one_eq_Ioi, prod_Ioi_zero, prod_Ici_succ, finsetImage_succ_Ici, Algebra.discr_powerBasis_eq_prod'', finsetImage_castSucc_Ici, Algebra.discr_powerBasis_eq_prod', map_castSuccEmb_Ioi, Ioi_sub_one_eq_Ici, Ioi_zero_eq_map, sum_Ioi_zero, finsetImage_natAdd_Ici, prod_prod_eq_prod_triangle_mul, map_revPerm_Iic, sum_Ioi_succ, finsetImage_rev_Ici, finsetImage_succ_Ioi, sum_Ici_succ, map_castAddEmb_Ioi
|