| Metric | Count |
|---|
DefinitionsIci, Ico, Iic, Iio, Ioc, Ioi, Ioo, uIcc, «term[[_,_]]», toLocallyFiniteOrder, toLocallyFiniteOrder, toLocallyFiniteOrderBot, toLocallyFiniteOrderTop, finsetIcc, finsetIco, finsetIoc, finsetIoo, ofFiniteIcc, ofIcc, ofIcc', ofOrderIsoClass, toLocallyFiniteOrderBot, toLocallyFiniteOrderTop, LocallyFiniteOrderBot, finsetIic, finsetIio, ofIic, ofIic', LocallyFiniteOrderTop, finsetIci, finsetIoi, ofIci, ofIci', elabFinsetBuilderIxx, instLocallyFiniteOrder, instLocallyFiniteOrderBot, instLocallyFiniteOrderTop, locallyFiniteOrder, locallyFiniteOrder, locallyFiniteOrderBot, locallyFiniteOrderTop, instLocallyFiniteOrder, instLocallyFiniteOrderBot, instLocallyFiniteOrderTop, fintypeUIcc, instFintypeIcc, instFintypeIci, instFintypeIco, instFintypeIic, instFintypeIio, instFintypeIoc, instFintypeIoi, instFintypeIoo, instLocallyFiniteOrder, instLocallyFiniteOrderBot, instLocallyFiniteOrderTop, insertBot, instLocallyFiniteOrder, insertTop, locallyFiniteOrder, instLocallyFiniteOrderBotSubtypeLeOfDecidableLEOfLocallyFiniteOrder, instLocallyFiniteOrderBotSubtypeLtOfDecidableLTOfLocallyFiniteOrder, instLocallyFiniteOrderTopSubtypeLeOfDecidableLEOfLocallyFiniteOrder, instLocallyFiniteOrderTopSubtypeLtOfDecidableLTOfLocallyFiniteOrder | 64 |
Theoremsfinite_of_bddAbove, Icc_ofDual, Icc_orderDual_def, Icc_prod_def, Icc_product_Icc, Icc_toDual, Ici_eq_Icc, Ici_ofDual, Ici_prod_def, Ici_product_Ici, Ici_toDual, Ico_ofDual, Ico_orderDual_def, Ico_toDual, Iic_eq_Icc, Iic_ofDual, Iic_prod_def, Iic_product_Iic, Iic_toDual, Iio_eq_Ico, Iio_ofDual, Iio_toDual, Ioc_ofDual, Ioc_orderDual_def, Ioc_toDual, Ioi_eq_Ioc, Ioi_ofDual, Ioi_toDual, Ioo_ofDual, Ioo_orderDual_def, Ioo_toDual, card_Icc_prod, card_Ici_prod, card_Iic_prod, card_uIcc_prod, coe_Icc, coe_Ici, coe_Ico, coe_Iic, coe_Iio, coe_Ioc, coe_Ioi, coe_Ioo, coe_uIcc, map_subtype_embedding_Icc, map_subtype_embedding_Ici, map_subtype_embedding_Ico, map_subtype_embedding_Iic, map_subtype_embedding_Iio, map_subtype_embedding_Ioc, map_subtype_embedding_Ioi, map_subtype_embedding_Ioo, mem_Icc, mem_Ici, mem_Ico, mem_Iic, mem_Iio, mem_Ioc, mem_Ioi, mem_Ioo, mem_uIcc, subtype_Icc_eq, subtype_Ici_eq, subtype_Ico_eq, subtype_Iic_eq, subtype_Iio_eq, subtype_Ioc_eq, subtype_Ioi_eq, subtype_Ioo_eq, uIcc_prod_def, uIcc_product_uIcc, card_Icc, card_Ici, card_Ico, card_Iic, card_Iio, card_Ioc, card_Ioi, card_Ioo, card_uIcc, Ici_orderDual_def, Iic_orderDual_def, Iio_orderDual_def, Ioi_orderDual_def, finset_mem_Icc, finset_mem_Ico, finset_mem_Ioc, finset_mem_Ioo, finset_mem_Iic, finset_mem_Iio, finset_mem_Ici, finset_mem_Ioi, finite_Icc, finite_Ici, finite_Ico, finite_Iic, finite_Iio, finite_Ioc, finite_Ioi, finite_Ioo, finite_iff_bddAbove, finite_iff_bddBelow, finite_iff_bddBelow_bddAbove, finite_interval, finite_uIcc, toFinset_Icc, toFinset_Ici, toFinset_Ico, toFinset_Iic, toFinset_Iio, toFinset_Ioc, toFinset_Ioi, toFinset_Ioo, Icc_bot_coe, Icc_coe_coe, Ico_bot_coe, Ico_coe_coe, Ioc_bot_coe, Ioc_coe_coe, Ioo_bot_coe, Ioo_coe_coe, bot_mem_insertBot, some_mem_insertBot, Icc_coe_coe, Icc_coe_top, Ico_coe_coe, Ico_coe_top, Ioc_coe_coe, Ioc_coe_top, Ioo_coe_coe, Ioo_coe_top, some_mem_insertTop, top_mem_insertTop, instFiniteSubtypeLeOfLocallyFiniteOrderBot, instFiniteSubtypeLeOfLocallyFiniteOrderTop, instFiniteSubtypeLtOfLocallyFiniteOrderBot, instFiniteSubtypeLtOfLocallyFiniteOrderTop, instSubsingletonLocallyFiniteOrder, instSubsingletonLocallyFiniteOrderBot, instSubsingletonLocallyFiniteOrderTop | 140 |
| Total | 204 |
| Name | Category | Theorems |
|---|
Ici 📖 | CompOp | 97 mathmath: Ici_succ_eq_Ioi_of_not_isMax, Icc_top, Sigma.Ici_mk, Fin.finsetImage_addNat_Ici, Pi.card_Ici, Fin.card_Ici, WithTop.Ico_coe_top, Fin.map_addNatEmb_Ici, Ioo_subset_Ici_self, Ioi_sub_one_eq_Ici_of_not_isMin, Ioi_insert, Fin.map_natAddEmb_Ici, mem_Ici, Fin.sum_sum_eq_sum_triangle_add, mul_prod_Ioi_eq_prod_Ici, Ioi_pred_eq_Ici_of_not_isMin, Fin.map_castAddEmb_Ici, Ici_eq_Icc, Ici_mul_Ioi_subset', Sum.Ici_inr, extDeriv_apply_vectorField, Fin.attachFin_Ico_eq_Ici, ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinCLM_comp_apply, Set.toFinset_Ici, Fintype.card_Ici, Fin.finsetImage_castAdd_Ici, Fin.finsetImage_cast_Ici, Fin.prod_Ici_cast, Ici_mul_Ici_subset', Ici_add_Ioi_subset, Fin.map_revPerm_Ici, inf'_Ici, Sum.Lex.Ici_inl, Fin.sum_Ici_cast, Ioi_sub_one_eq_Ici, Fin.finsetImage_rev_Iic, AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, Icc_subset_Ici_self, Fin.map_valEmbedding_Ici, Fin.map_finCongr_Ici, Ici_add_one_eq_Ioi_of_not_isMax, Ioc_subset_Ici_self, Ici_bot, Ici_succ_eq_Ioi, Iic_orderDual_def, Fin.map_succEmb_Ici, Fin.finsetImage_val_Ici, Fin.map_castSuccEmb_Ici, sum_Ioi_add_eq_sum_Ici, extDerivWithin_apply_vectorField, Sum.Lex.Ici_inr, Ioi_pred_eq_Ici, Sum.Ici_inl, Ici_prod_def, card_Ioi_eq_card_Ici_sub_one, Ici_toDual, Sum.Lex.Ico_inl_inr, add_sum_Ioi_eq_sum_Ici, Ici_eq_cons_Ioi, Ici_product_Ici, Iic_ofDual, map_subtype_embedding_Ici, Ici_ssubset_Ici, nonempty_Ici, Ioi_add_Ici_subset, Ici_add_Ici_subset, Fin.Ici_add_one_eq_Ioi, SummationFilter.conditional_filter_eq_map_Ici, prod_Ioi_mul_eq_prod_Ici, Fin.prod_Ici_succ, Ioi_subset_Ici_self, Fin.finsetImage_succ_Ici, Filter.tendsto_finset_Ici_atBot_atTop, Fin.finsetImage_castSucc_Ici, Iic_toDual, Ici_orderDual_def, card_Ici_prod, Fin.Ioi_sub_one_eq_Ici, coe_Ici, subtype_Ici_eq, Ico_subset_Ici_self, WithTop.Icc_coe_top, Fin.finsetImage_natAdd_Ici, Ici_add_one_eq_Ioi, inf_Ici, Sum.Lex.Icc_inl_inr, Fin.prod_prod_eq_prod_triangle_mul, Fin.map_revPerm_Iic, Ici_subset_Ici, Fin.finsetImage_rev_Ici, Pi.card_Ioi, filter_le_eq_Ici, Ici_top, Fin.sum_Ici_succ, Ioi_mul_Ici_subset', Ici_ofDual, Ici_erase
|
Ico 📖 | CompOp | 336 mathmath: insert_Ico_succ_left_eq_Ico, sum_Ico_add_eq_sum_Ico_add_one, sum_Ico_sub_bot, Ico_bot, insert_Ico_left_eq_Ico_pred, eVariationOn.sum_le_of_monotoneOn_Icc, sum_Ico_Ico_comm', FormalMultilinearSeries.comp_partialSum, Ico_subset_Ico_right, sum_Ico_eq_add_neg, PNat.map_subtype_embedding_Ico, Ico_eq_empty, WithTop.Ico_coe_coe, Fin.Ico_add_one_eq_Ioo, insert_Ico_add_one_left_eq_Ico, Fin.map_revPerm_Ioc, Fin.map_castAddEmb_Ico, Ico_subset_Ico_union_Ico, coe_Ico, tendsto_Ico_neg_atTop_atTop, Finsupp.card_Ico, card_Ico_mul_right, Nat.Ico_succ_left_eq_erase_Ico, sum_range_add_sum_Ico, Nat.image_Ico_mod, Icc_sub_one_right_eq_Ico_of_not_isMin, Ico_filter_le_of_left_le, Fin.prod_Ico_succ, WithTop.Ico_coe_top, Sum.Lex.Ico_inl_inl, Sum.Lex.Ico_inr_inr, Ico_succ_right_eq_Icc_of_not_isMax, prod_Ico_consecutive, Nat.image_sub_const_Ico, prod_Icc_eq_prod_Ico_mul, edist_le_Ico_sum_of_edist_le, prod_range_mul_prod_Ico, Multiset.card_Ico, sum_Ico_le_sum, Sum.Ico_inl_inl, prod_Ico_mul_eq_prod_Ico_add_one, sum_Ico_sub, sum_condensed_le, sum_Ico_int_sub, insert_Ico_right_eq_Ico_add_one_of_not_isMax, subtype_Ico_eq, card_Ico_add_right, Ico_filter_le_of_le_left, Nat.Ico_image_const_sub_eq_Ico, List.toFinset_range'_1, Ico_self, prod_Ico_reflect, Nat.factorization_factorial, Nat.Prime.emultiplicity_factorial, Fin.sum_Ico_castSucc, Nat.Ico_pow_dvd_eq_Ico_of_lt, Iio_eq_Ico, Ioc_ofDual, Ico_diff_Ico_left, le_sum_condensed', Ico_filter_le_left, Fin.map_castAddEmb_Ici, Icc_pred_right_eq_Ico_of_not_isMin, Ico_add_one_right_eq_Icc_of_not_isMax, Ico_union_Ico', Fin.finsetImage_castLE_Ico, Nat.factorization_eq_card_pow_dvd_of_lt, AkraBazziRecurrence.sumTransform_def, Ico_disjoint_Ico_consecutive, Fin.finsetImage_succ_Ico, insert_Ico_left_eq_Ico_sub_one_of_not_isMin, sum_Ioo_add_eq_sum_Ico, insert_Ico_left_eq_Ico_pred_of_not_isMin, sum_Ico_eq_sub, insert_Ico_sub_one_right_eq_Ico, MonotoneOn.integral_le_sum_Ico, le_sum_schlomilch', Fin.map_revPerm_Ico, Icc_subset_Ico_iff, Fin.finsetImage_castAdd_Ico, WithBot.Ico_bot_coe, integral_le_sum_mul_Ico_of_antitone_monotone, PNat.Ico_eq_finset_subtype, Ico_subset_Ico_left, Fin.attachFin_Ico_eq_Ici, prod_Ico_mul_eq_prod_Icc, Ico_add_one_left_eq_Ioo, primorial_add, Fin.card_Ico, Ico_inter_Ico_consecutive, filter_le_lt_eq_Ico, Fin.map_castLEEmb_Ico, Ico_insert_right, Fin.sum_Ico_succ, Sigma.Ico_mk_mk, Set.toFinset_Ico, sum_schlomilch_le, Ico_eq_filter_ssubsets, Fin.Ico_add_one_eq_Icc, IncidenceAlgebra.mu_apply, Fin.finsetImage_castAdd_Ici, prod_Ico_int_div, Nat.Prime.emultiplicity_choose', Int.card_Ico_of_le, Ico_inter_Ico, Ico_filter_lt_of_le_right, prod_Ico_add', ZMod.sum_mul_div_add_sum_mul_div_eq_mul, padicValNat_choose', Nat.Prime.pow_dvd_factorial_iff, Fin.finsetImage_castSucc_Ico, sum_Ico_le_integral_of_le, SummationFilter.symmetricIco_filter, card_Ico_one_mul, Icc_subset_Ico_right, geom_sum_Ico_mul, geom_sum_Ico_mul_neg, sum_Ico_succ_top, tendsto_Ico_atBot_prod_atTop, intervalIntegral.sum_integral_adjacent_intervals_Ico, map_add_left_Ico, AntitoneOn.sum_le_integral_Ico, Nat.Prime.emultiplicity_choose, sum_Icc_eq_sum_Ico_add, Int.card_Ico, Ico_erase_left, Ioc_sub_one_sub_one_eq_Ico_of_not_isMin, Int.image_Ico_emod, Fin.map_addNatEmb_Ico, Fin.map_valEmbedding_Ici, MonotoneOn.sum_le_integral_Ico, Icc_sub_one_right_eq_Ico, Ico_eq_image_ssubsets, Ioc_sub_one_sub_one_eq_Ico, Fin.finsetImage_rev_Ioc, sum_mul_Ico_le_integral_of_monotone_antitone, Ico_filter_lt_of_right_le, Ico_add_Icc_subset, Nat.Ico_filter_modEq_card, Ico_filter_le_of_right_le, card_Ico_zero_add, Ico_union_Ico_eq_Ico, card_Ico_finset, sum_Ico_pow, sum_Ico_by_parts, Fin.finsetImage_natAdd_Ico, Ico_mul_Icc_subset', PNat.card_Ico, Fin.sum_Ico_cast, Ioc_mul_Ico_subset', Fin.finsetImage_val_Ico, Int.Ico_filter_dvd_card, Fin.prod_Ico_cast, Nat.multiplicity_choose_aux, Ico_succ_succ, Commute.geom_sum₂_Ico, AntitoneOn.integral_le_sum_Ico, Icc_pred_right_eq_Ico, mul_prod_Ico_eq_prod_Icc, prod_Ico_id_eq_factorial, sum_Ico_Ico_comm, Fin.finsetImage_val_Ici, Icc_erase_right, Ico_ofDual, Ioc_orderDual_def, Nat.Ico_filter_modEq_cast, Nat.card_Ico, Fin.map_castSuccEmb_Ici, Nat.Ico_pred_singleton, prod_Ioo_mul_eq_prod_Ico, Fin.attachFin_Ico, Nat.factorization_choose', Ico_union_Ico, sum_Ico_add_right_sub_eq, Fin.finsetImage_addNat_Ico, ZMod.gauss_lemma, Ioc_toDual, Fin.map_natAddEmb_Ico, sum_Ico_add', Ico_add_one_right_eq_Icc, Ioc_pred_pred_eq_Ico, Nat.Icc_factorization_eq_pow_dvd, SummationFilter.hasProd_symmetricIco_int_iff, SummationFilter.hasSum_symmetricIco_int_iff, Ico_subset_Iic_self, prod_eq_prod_Ico_succ_bot, right_notMem_Ico, Ioo_pred_left_eq_Ioc, sum_eq_sum_Ico_succ_bot, gaussSum_pow_eq_prod_jacobiSum_aux, prod_Ico_eq_div, Pi.card_Ico, card_Ico_eq_card_Icc_sub_one, Ico_subset_Ico_iff, Sum.Lex.Ico_inr_inl, PowerSeries.trunc_apply, Ico_filter_le, sum_Ico_eq_sum_range, map_add_right_Ico, insert_Ico_right_eq_Ico_add_one, Nat.Ico_eq_range', Sum.Lex.Ico_inl_inr, padicValNat_choose, mul_prod_Ioo_eq_prod_Ico, padicValNat_factorial, sum_Ico_add, mul_geom_sum₂_Ico, Icc_mul_Ico_subset', Fin.prod_Ico_castSucc, MeasureTheory.upcrossingsBefore_eq_sum, Ico_eq_empty_of_le, MeasureTheory.stoppedValue_sub_eq_sum, Icc_diff_Ico_self, Ico_add_Ioc_subset, prod_Ico_succ_top, Nat.Ico_filter_coprime_le, sum_Ico_succ_sub_top, ZMod.Ico_map_valMinAbs_natAbs_eq_Ico_map_id, Nat.Ico_succ_right_eq_insert_Ico, image_add_right_Ico, Sum.Ico_inr_inr, Fin.map_valEmbedding_Ico, sum_Ico_consecutive, EisensteinSeries.tendsto_double_sum_S_act, Nat.filter_coprime_Ico_eq_totient, Fin.Icc_sub_one_eq_Ico, Fin.map_succEmb_Ico, Ico_subset_Iio_self, Nat.Ico_zero_eq_range, card_Ioo_eq_card_Ico_sub_one, DFinsupp.card_Ico, prod_Ico_div, FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1, Int.Ico_filter_modEq_card, Ioo_sub_one_left_eq_Ioc, Ico_diff_Ico_right, ZMod.gauss_lemma_aux, Ico_add_one_add_one_eq_Ioc_of_not_isMax, Nat.Ico_filter_pow_dvd_eq, Ico_subset_Icc_self, insert_Ico_right_eq_Ico_succ, Fin.sum_Ico_castAdd, Sigma.card_Ico, gaussSum_pow_eq_prod_jacobiSum, Ico_orderDual_def, Nat.factorization_eq_card_pow_dvd, Sum.Ico_inl_inr, Int.Ico_eq_finset_map, Ioc_pred_pred_eq_Ico_of_not_isMin, integral_le_sum_Ico_of_le, geom_sum_Ico', Ico_filter_lt_of_le_left, Icc_eq_cons_Ico, Fin.prod_Ico_castLE, range_eq_Ico, WithBot.Ico_coe_coe, Fin.Ioo_sub_one_eq_Ico, Ico_eq_cons_Ioo, Ioo_insert_left, Ico_diff_Ioo_self, Ico_map_sectR, Nat.Ico_succ_singleton, sum_Ico_reflect, prod_Ico_succ_div_top, tendsto_Ico_neg, Ioo_sub_one_left_eq_Ioc_of_not_isMin, prod_Ico_div_bot, EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq, Commute.mul_geom_sum₂_Ico, Ico_succ_succ_eq_Ioc_of_not_isMax, sum_Ico_add_eq_sum_Icc, Ioc_add_Ico_subset, ZMod.eisenstein_lemma, Fin.finsetImage_castSucc_Ici, Icc_add_Ico_subset, Fin.finsetImage_rev_Ico, Ico_succ_left_eq_Ioo, map_subtype_embedding_Ico, Ioo_subset_Ico_self, FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2, Fin.map_castSuccEmb_Ico, Ico_filter_lt, prod_Ico_eq_prod_range, Fintype.card_Ico, Ico_eq_empty_iff, addRothNumber_Ico, Nat.factorization_choose, sum_schlomilch_le', Ico_map_sectL, IncidenceAlgebra.mu_eq_neg_sum_Ico_of_ne, Ico_subset_Ioo_left, nonempty_Ico, Int.Ico_filter_modEq_eq, dist_le_Ico_sum_of_dist_le, edist_le_Ico_sum_edist, insert_Ico_pred_right_eq_Ico, Ioo_pred_left_eq_Ioc_of_not_isMin, Ico_subset_Ici_self, ZMod.prod_Ico_one_prime, Fin.sum_Ico_castLE, geom_sum_Ico, add_sum_Ico_eq_sum_Icc, geom_sum₂_Ico, image_add_left_Ico, Fin.finsetImage_cast_Ico, Ico_mul_Ioc_subset', insert_Ico_left_eq_Ico_sub_one, insert_Ico_right_eq_Ico_succ_of_not_isMax, prod_Ico_add_right_sub_eq, add_sum_Ioo_eq_sum_Ico, Nat.emultiplicity_eq_card_pow_dvd, ZMod.eisenstein_lemma_aux, Nat.mod_injOn_Ico, Commute.geom_sum₂_Ico_mul, dist_le_Ico_sum_dist, Ico_succ_succ_eq_Ioc, Int.Ico_filter_dvd_eq, ZMod.div_eq_filter_card, geom_sum_Ico_le_of_lt_one, sum_condensed_le', prod_range_eq_mul_Ico, Nat.geom_sum_Ico_le, Ico_toDual, Fin.map_finCongr_Ico, Aesop.nonempty_Ico_of_lt, Sum.Ico_inr_inl, prod_Ico_eq_mul_inv, mem_Ico, sum_range_eq_add_Ico, left_mem_Ico, Ico_succ_right_eq_Icc, prod_Ico_add, Nat.filter_Ico_card_eq_of_periodic, Ico_subset_Ico, Ico_add_one_add_one_eq_Ioc, Fin.prod_Ico_castAdd
|
Iic 📖 | CompOp | 158 mathmath: SchwartzMap.norm_toLp_le_seminorm, partialSups_apply, Fin.attachFin_Iic, ProbabilityTheory.Kernel.partialTraj_succ_of_le, Icc_subset_Iic_self, Nat.largeSchroder_succ, Fin.map_castLEEmb_Iic, card_Iic_prod, Pi.card_Iic, coe_Iic, sup'_Iic, MeasureTheory.isProjectiveLimit_nat_iff, Sum.Lex.Iic_inr, Fintype.card_Iic, Ioc_subset_Iic_self, Fin.sum_Iic_cast, Set.toFinset_Iic, Fin.finsetImage_castAdd_Iic, Nat.range_succ_eq_Iic, Sigma.Iic_mk, Iic_union_Ioc_eq_Iic, WithBot.Ioc_bot_coe, Fin.sum_Iic_castAdd, Iic_sub_one_eq_Iio_of_not_isMin, MeasurableEquiv.coe_IicProdIoc_symm, Fin.map_finCongr_Iic, mem_Iic, Iic_add_Iic_subset, biUnion_slice, Iio_succ_eq_Iic_of_not_isMax, sup_Iic, Fin.map_revPerm_Ici, card_Iio_eq_card_Iic_sub_one, ProbabilityTheory.Kernel.partialTraj_succ_eq_comp, Preorder.measurable_frestrictLe₂, Preorder.continuous_frestrictLe, sum_card_slice, DFinsupp.card_Iic, Iic_top, ProbabilityTheory.Kernel.partialTraj_le_def, add_sum_Iio_eq_sum_Iic, Fin.sum_Iic_castLE, Iic_bot, Pi.card_Iio, Fin.finsetImage_rev_Iic, Preorder.frestrictLe_updateFinset, Sum.Lex.Ioc_inl_inr, IicProdIoc_def, Iic_eq_Icc, MeasureTheory.inducedFamily_Iic, MeasureTheory.Measure.pi_prod_map_IicProdIoc, Nat.card_Iic, MeasureTheory.measurableCylinders_nat, Iic_mul_Iic_subset', Iio_add_one_eq_Iic, ProbabilityTheory.Kernel.instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj, Iic_pred_eq_Iio, MeasureTheory.partialTraj_const, Fin.prod_Iic_castSucc, ProbabilityTheory.Kernel.partialTraj_le, Fin.finsetImage_succ_Iic, ProbabilityTheory.Kernel.partialTraj_succ_self, WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, Iic_orderDual_def, Iio_succ_eq_Iic, Preorder.frestrictLe_updateFinset_of_le, Iic_ssubset_Iic, measurable_IicProdIoc, image_subset_Iic_sup, Iic_eq_cons_Iio, Iic_eq_powerset, MeasurableEquiv.coe_IicProdIoc, Preorder.frestrictLe_apply, biUnion_Iic_disjointed, Preorder.frestrictLe₂_apply, Iic_erase, Fin.prod_Iic_cast, Sum.Lex.Iic_inl, Iio_subset_Iic_self, Iic_mul_Iio_subset', Ico_subset_Iic_self, SchwartzMap.eLpNorm_le_seminorm, ProbabilityTheory.Kernel.partialTraj_comp_partialTraj, Iic_subset_Iic, Iic_disjoint_Ioc, prod_Iio_mul_eq_prod_Iic, Ici_toDual, Iic_pred_eq_Iio_of_not_isMin, Sum.Iic_inl, Iio_mul_Iic_subset', Iio_add_one_eq_Iic_of_not_isMax, Fin.Iio_add_one_eq_Iic, ProbabilityTheory.Kernel.partialTraj_self, Iic_ofDual, Fin.card_Iic, filter_ge_eq_Iic, IicProdIoc_preimage, Fin.finsetImage_castSucc_Iic, Sum.Iic_inr, Iio_add_Iic_subset, Fin.prod_Iic_castLE, Iic_add_Iio_subset, Fin.map_castSuccEmb_Iic, card_Iic_finset, Finsupp.card_Iic, Icc_bot, Fin.Iic_sub_one_eq_Iio, Finsupp.card_Iio, MeasureTheory.stoppedValue_eq', Preorder.measurable_frestrictLe, Ioo_subset_Iic_self, MeasureTheory.partialTraj_const_restrict₂, MeasureTheory.Filtration.piLE_eq_comap_frestrictLe, Fin.sum_Iic_castSucc, mul_prod_Iio_eq_prod_Iic, Iio_insert, Multiset.card_Iic, Fin.finsetImage_val_Iic, Fin.finsetImage_castLE_Iic, card_shatterer_le_sum_vcDim, Preorder.updateFinset_frestrictLe, Iic_toDual, Iic_sub_one_eq_Iio, WithSeminorms.partial_sups, Ici_orderDual_def, sum_Iio_add_eq_sum_Iic, Iic_product_Iic, Fin.finsetImage_cast_Iic, subtype_Iic_eq, IicProdIoc_comp_restrict₂, RootPairing.Base.exists_eq_sum_and_forall_sum_mem_of_isPos, subset_Iic_sup_id, Fin.map_castAddEmb_Iic, Fin.prod_Iic_castAdd, Iic_filter_lt_of_lt_right, Preorder.piCongrLeft_comp_restrictLe, Filter.tendsto_finset_Iic_atTop_atTop, Iic_prod_def, DFinsupp.card_Iio, ProbabilityTheory.Kernel.partialTraj_zero, Sum.Lex.Icc_inl_inr, SchwartzMap.one_add_le_sup_seminorm_apply, Preorder.piCongrLeft_comp_frestrictLe, Fin.map_revPerm_Iic, Iic_diff_Ioc, SummationFilter.conditional_filter_eq_map_Iic, Preorder.continuous_frestrictLe₂, disjiUnion_Iic_disjointed, Fin.map_succEmb_Iic, Fin.finsetImage_rev_Ici, map_subtype_embedding_Iic, WithBot.Icc_bot_coe, Fin.map_valEmbedding_Iic, Iic_diff_Ioc_self_of_le, nonempty_Iic, MeasureTheory.isProjectiveLimit_nat_iff', Ici_ofDual, restrict₂_comp_IicProdIoc
|
Iio 📖 | CompOp | 106 mathmath: Fin.finsetImage_castLE_Iio, Ico_bot, Fin.map_succEmb_Iio, Ioi_disjUnion_Iio, Iio_filter_lt, Ioi_toDual, Iio_ssubset_Iio, Sum.Lex.Ioo_inl_inr, Fin.finsetImage_castAdd_Iio, InnerProductSpace.gramSchmidt_def, Sum.Iio_inr, Iio_eq_Ico, Aesop.nonempty_Iio_of_not_isMin, Fin.finsetImage_succ_Iio, Iic_sub_one_eq_Iio_of_not_isMin, WithBot.Ico_bot_coe, card_Iio_finset, IsMin.finsetIio_eq, subtype_Iio_eq, Fin.finsetImage_cast_Iio, Fin.finsetImage_val_Iio, Iio_orderDual_def, Fin.addRothNumber_eq_rothNumberNat, Iio_succ_eq_Iic_of_not_isMax, Equiv.Perm.sign_eq_prod_prod_Iio, card_Iio_eq_card_Iic_sub_one, Sum.Iio_inl, Iio_nonempty, add_sum_Iio_eq_sum_Iic, Pi.card_Iio, Fin.sum_Iio_castLE, Sum.Lex.Iio_inl, Fin.map_revPerm_Ioi, Fin.Iio_last_eq_map, Fin.prod_Iio_castSucc, Iio_add_one_eq_Iic, Ioi_orderDual_def, Iic_pred_eq_Iio, Fin.finsetImage_rev_Ioi, disjoint_Ioi_Iio, Fin.prod_Iio_castAdd, Iio_succ_eq_Iic, Sigma.Iio_mk, Fin.card_Iio, Iic_eq_cons_Iio, InnerProductSpace.gramSchmidt_def', nonempty_Iio, Iic_erase, MeasureTheory.stoppedProcess_eq'', Iio_subset_Iic_self, Iic_mul_Iio_subset', Ioi_ofDual, prod_Iio_mul_eq_prod_Iic, Sum.Lex.Ico_inl_inr, Iic_pred_eq_Iio_of_not_isMin, Fin.map_castLEEmb_Iio, Sum.Lex.Iio_inr, Iio_mul_Iic_subset', InnerProductSpace.gramSchmidt_def'', Fin.sum_Iio_castAdd, map_subtype_embedding_Iio, Iio_add_one_eq_Iic_of_not_isMax, Iio_toDual, Fin.sum_Iio_cast, Fin.Iio_castSucc, Fin.map_castAddEmb_Iio, Fin.Iio_add_one_eq_Iic, Fin.sum_Iio_castSucc, Fin.attachFin_Iio, Fin.map_castSuccEmb_Iio, Fin.map_revPerm_Iio, Fin.addRothNumber_le_rothNumberNat, notMem_Iio_self, Iio_add_Iic_subset, Ico_subset_Iio_self, Fin.finsetImage_rev_Iio, Iic_add_Iio_subset, Fin.Iic_sub_one_eq_Iio, coe_Iio, Finsupp.card_Iio, Iio_bot, disjointed_apply, Fin.prod_Iio_cast, Fin.map_valEmbedding_univ, mul_prod_Iio_eq_prod_Iic, Iio_subset_Iio, Iio_insert, Fintype.card_Iio, Iio_eq_ssubsets, Fin.prod_Iio_castLE, Iic_sub_one_eq_Iio, Nat.card_Iio, sum_Iio_add_eq_sum_Iic, Fin.finsetImage_castSucc_Iio, WithBot.Ioo_bot_coe, mem_Iio, Fin.map_finCongr_Iio, Ioo_subset_Iio_self, filter_gt_eq_Iio, Fin.map_valEmbedding_Iio, DFinsupp.card_Iio, Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod, Set.toFinset_Iio, Nat.Iio_eq_range, Iio_ofDual, Iio_eq_empty
|
Ioc 📖 | CompOp | 233 mathmath: Fin.finsetImage_natAdd_Ioc, prod_Ioo_mul_eq_prod_Ioc, Finsupp.card_Ioc, Fin.map_castLEEmb_Ioc, Ioc_sub_one_left_eq_Icc_of_not_isMin, Fin.map_revPerm_Ioc, Icc_add_one_left_eq_Ioc, Nat.Ioc_filter_modEq_cast, Nat.Ioc_succ_singleton, ProbabilityTheory.Kernel.partialTraj_succ_of_le, IocProdIoc_preimage, Icc_erase_left, WithTop.Ioc_coe_coe, ArithmeticFunction.sum_Ioc_mul_zeta_eq_sum, subtype_Ioc_eq, Ioc_union_Ioc_eq_Ioc, Ioc_erase_right, schnirelmannDensity_le_iff_forall, Ioo_add_one_right_eq_Ioc_of_not_isMax, right_mem_Ioc, le_schnirelmannDensity_iff, insert_Ioc_right_eq_Ioc_add_one, tendsto_Ioc_neg_atTop_atTop, Ioc_subset_Iic_self, Fin.finsetImage_castSucc_Ioc, exists_of_schnirelmannDensity_eq_zero, Ioc_ofDual, Chebyshev.psi_sub_theta_eq_sum_not_prime, Icc_succ_left_eq_Ioc_of_not_isMax, Sum.Ioc_inl_inr, mul_prod_Ioo_eq_prod_Ioc, Icc_subset_Ioc_iff, Iic_union_Ioc_eq_Iic, WithBot.Ioc_bot_coe, sup_Ioc_disjointed_of_monotone, MeasurableEquiv.coe_IicProdIoc_symm, Icc_diff_Ioc_self, Fin.map_revPerm_Ico, MeasureTheory.Measure.map_piSingleton, sum_Ioc_add_eq_sum_Icc, Ioc_sub_one_left_eq_Icc, Int.card_Ioc, Fin.Ioo_add_one_eq_Ioc, tendsto_Ioc_atBot_prod_atTop, MeasureTheory.Measure.pi_prod_map_IocProdIoc, mul_prod_Ioc_eq_prod_Icc, SummationFilter.hasSum_symmetricIoc_int_iff, Multiset.card_Ioc, Sum.Ioc_inr_inr, Nat.Ioc_filter_dvd_card_eq_div, Chebyshev.sum_PrimePow_eq_sum_sum, Pi.card_Ioc, Nat.Ioc_eq_range', Fin.sum_Ioc_castAdd, Ioc_eq_cons_Ioo, Fin.prod_Ioc_castLE, Fin.finsetImage_addNat_Ioc, insert_Ioc_succ_left_eq_Ioc, insert_Ioc_right_eq_Ioc_succ_of_not_isMax, Sum.Lex.Ioc_inl_inl, ProbabilityTheory.Kernel.partialTraj_le_def, SummationFilter.symmetricIoc_filter, Ioc_diff_Ioo_self, Fin.prod_Ioc_castSucc, Ioc_inter_Ioc, insert_Ioc_pred_right_eq_Ioc, Set.toFinset_Ioc, coe_Ioc, Ioc_sub_one_right_eq_Ioo, Nat.Ioc_filter_modEq_card, Int.Ioc_filter_modEq_card, Fin.sum_Ioc_castLE, Sum.Lex.Ioc_inl_inr, add_sum_Ioc_eq_sum_Icc, Ioo_succ_right_eq_Ioc, IicProdIoc_def, Fin.finsetImage_val_Ioc, MeasureTheory.Measure.pi_prod_map_IicProdIoc, Int.card_Ioc_of_le, Ioc_sub_one_sub_one_eq_Ico_of_not_isMin, Ioc_succ_succ, Ioi_eq_Ioc, insert_Ioc_right_eq_Ioc_succ, Ioo_succ_right_eq_Ioc_of_not_isMax, Ioc_map_sectL, Icc_add_one_left_eq_Ioc_of_not_isMax, Icc_eq_cons_Ioc, Ioc_sub_one_sub_one_eq_Ico, Fin.finsetImage_rev_Ioc, Sum.Lex.Ioc_inr_inl, Ioc_eq_empty, MeasureTheory.partialTraj_const, Fin.finsetImage_succ_Iic, Sum.Lex.Ioc_inr_inr, Ioc_subset_Ici_self, ProbabilityTheory.Kernel.partialTraj_succ_self, Ioc_eq_empty_iff, Ioc_self, Ioc_mul_Ico_subset', Ioc_subset_Icc_self, insert_Ioc_left_eq_Ioc_pred_of_not_isMin, sum_Ioo_add_eq_sum_Ioc, ArithmeticFunction.sum_Ioc_zeta, ArithmeticFunction.sum_Ioc_mul_eq_sum_prod_filter, measurable_IicProdIoc, Int.Ioc_eq_finset_map, PNat.Ioc_eq_finset_subtype, Ioc_pred_right_eq_Ioo, MeasurableEquiv.coe_IicProdIoc, Ico_ofDual, Nat.mem_Ioc_succ', Ioc_orderDual_def, card_Ioc_eq_card_Icc_sub_one, map_subtype_embedding_Ioc, Ioc_toDual, schnirelmannDensity_le_div, card_Ioo_eq_card_Ioc_sub_one, Ioc_pred_pred_eq_Ico, Sigma.Ioc_mk_mk, Ioc_subset_Ioi_self, add_sum_Ioo_eq_sum_Ioc, sum_Ioc_succ_top, Iic_disjoint_Ioc, Fin.map_castAddEmb_Ioc, Aesop.nonempty_Ioc_of_lt, Icc_succ_left_eq_Ioc, IncidenceAlgebra.mu_eq_neg_sum_Ioc_of_ne, Ioc_map_sectR, Ioo_insert_right, Ioc_pred_left_eq_Icc_of_not_isMin, Ioc_disjoint_Ioc_of_le, Ioc_insert_left, prod_Ioc_mul_eq_prod_Icc, Ioc_filter_lt_of_lt_right, Ico_add_Ioc_subset, Fin.Ioc_sub_one_eq_Icc, map_add_left_Ioc, Ioo_add_one_right_eq_Ioc, map_add_right_Ioc, Ioo_subset_Ioc_self, Ioc_pred_left_eq_Icc, insert_Ioc_left_eq_Ioc_sub_one, IicProdIoc_preimage, left_notMem_Ioc, Nat.divisorsAntidiagonal_eq_prod_filter_of_le, card_Ioc_finset, Fin.prod_Ioc_castAdd, prod_Ioc_consecutive, Int.Ioc_filter_dvd_eq, Fin.map_addNatEmb_Ioc, Fin.map_succEmb_Ioc, Ico_add_one_add_one_eq_Ioc_of_not_isMax, Fin.sum_Ioc_succ, insert_Ioc_sub_one_right_eq_Ioc, Nat.card_Ioc, Ioc_subset_Ioc, Fin.sum_Ioc_cast, Sigma.card_Ioc, Ico_orderDual_def, Ioc_pred_pred_eq_Ico_of_not_isMin, MeasureTheory.partialTraj_const_restrict₂, Fintype.card_Ioc, insert_Ioc_left_eq_Ioc_pred, Ioc_subset_Ioo_right, schnirelmannDensity_lt_iff, image_add_right_Ioc, filter_lt_le_eq_Ioc, sum_Ioc_inv_sq_le_sub, Ioc_eq_filter_powerset, PNat.card_Ioc, Ico_succ_succ_eq_Ioc_of_not_isMax, Polynomial.Monic.irreducible_iff_natDegree', Ioc_add_Ico_subset, Fin.Ioc_sub_one_eq_Ioo, tendsto_Ioc_neg, Fin.card_Ioc, sum_Ioc_by_parts, mem_Ioc, prod_Ioc_succ_top, Fin.finsetImage_rev_Ico, WithTop.Ioc_coe_top, ArithmeticFunction.sum_Ioc_sigma0_eq_sum_div, measurable_IocProdIoc, sum_mul_eq_sub_sub_integral_mul', Fin.finsetImage_castLE_Ioc, IicProdIoc_comp_restrict₂, Fin.prod_Ioc_succ, Ioc_eq_empty_of_le, Int.Ioc_filter_modEq_eq, Ioc_subset_Ioc_right, Ioc_disjoint_Ioc, ArithmeticFunction.sum_Ioc_mul_eq_sum_sum, WithBot.Ioc_coe_coe, Fin.finsetImage_cast_Ioc, Fin.map_finCongr_Ioc, Fin.Icc_add_one_eq_Ioc, Ico_mul_Ioc_subset', Sum.Ioc_inr_inl, PNat.map_subtype_embedding_Ioc, Fin.sum_Ioc_castSucc, Fin.finsetImage_succ_Ioc, Sum.Ioc_inl_inl, Fin.finsetImage_castAdd_Ioc, Ioc_top, ProbabilityTheory.Kernel.lmarginalPartialTraj_eq_lintegral_map, Fin.map_natAddEmb_Ioc, sum_mul_eq_sub_sub_integral_mul, Nat.mem_Ioc_succ, Fin.map_castSuccEmb_Ioc, Iic_diff_Ioc, SummationFilter.hasProd_symmetricIoc_int_iff, Ico_succ_succ_eq_Ioc, image_add_left_Ioc, sum_le_sum_Ioc, nonempty_Ioc, insert_Ioc_add_one_left_eq_Ioc, Fin.map_succEmb_Iic, schnirelmannDensity_mul_le_card_filter, insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin, Fin.prod_Ioc_cast, sum_Ioc_consecutive, Ico_toDual, DFinsupp.card_Ioc, biUnion_Ioc_disjointed_of_monotone, Int.Ioc_filter_dvd_card, Iic_diff_Ioc_self_of_le, insert_Ioc_right_eq_Ioc_add_one_of_not_isMax, ProbabilityTheory.Kernel.partialTraj_eq_prod, Fin.map_valEmbedding_Ioc, Fin.attachFin_Ioc, Ioc_subset_Ioc_left, Ico_add_one_add_one_eq_Ioc, restrict₂_comp_IicProdIoc
|
Ioi 📖 | CompOp | 98 mathmath: Fin.card_Ioi, Ici_succ_eq_Ioi_of_not_isMax, notMem_Ioi_self, Fin.Ioi_succ, Ioi_disjUnion_Iio, Fin.finsetImage_addNat_Ioi, Ioi_toDual, Fin.finsetImage_val_Ioi, Matrix.det_vandermonde, Sum.Lex.Ioo_inl_inr, Fin.attachFin_Ioo_eq_Ioi, Set.toFinset_Ioi, Ioi_sub_one_eq_Ici_of_not_isMin, Ioi_insert, WithTop.Ioo_coe_top, Matrix.det_projVandermonde, mul_prod_Ioi_eq_prod_Ici, Equiv.Perm.sign_eq_prod_prod_Ioi, Fin.map_addNatEmb_Ioi, Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod, Ioi_pred_eq_Ici_of_not_isMin, Ioi_ssubset_Ioi, Ici_mul_Ioi_subset', Fin.finsetImage_cast_Ioi, Fin.sum_Ioi_cast, Sum.Lex.Ioi_inr, Sum.Ioi_inr, Iio_orderDual_def, Ioi_nonempty, Ici_add_Ioi_subset, filter_lt_eq_Ioi, Ioi_sub_one_eq_Ici, Sum.Lex.Ioc_inl_inr, Fin.map_revPerm_Ioi, Ioi_eq_Ioc, map_subtype_embedding_Ioi, Ioi_orderDual_def, Fin.map_succEmb_Ioi, Ioi_eq_empty, Fin.finsetImage_rev_Ioi, Ici_add_one_eq_Ioi_of_not_isMax, disjoint_Ioi_Iio, Fin.prod_Ioi_cast, Fin.finsetImage_castAdd_Ioi, Ici_succ_eq_Ioi, Sum.Lex.Ioi_inl, Fin.prod_Ioi_succ, prod_prod_Ioi_mul_eq_prod_prod_off_diag, Aesop.nonempty_Ioi_of_not_isMax, sum_Ioi_add_eq_sum_Ici, mem_Ioi, Ioc_subset_Ioi_self, Ioi_pred_eq_Ici, Sigma.Ioi_mk, Ioi_ofDual, Algebra.discr_powerBasis_eq_prod, card_Ioi_eq_card_Ici_sub_one, Fin.finsetImage_castSucc_Ioi, Fin.map_valEmbedding_Ioi, Fin.finsetImage_natAdd_Ioi, add_sum_Ioi_eq_sum_Ici, sum_sum_Ioi_add_eq_sum_sum_off_diag, Iio_toDual, Ici_eq_cons_Ioi, Ioi_subset_Ioi, coe_Ioi, Fin.map_natAddEmb_Ioi, Fin.map_revPerm_Iio, Fin.finsetImage_rev_Iio, Ioi_add_Ici_subset, Fin.map_finCongr_Ioi, Fin.Ici_add_one_eq_Ioi, Fin.prod_Ioi_zero, prod_Ioi_mul_eq_prod_Ici, Ioi_top, Ioi_subset_Ici_self, Fintype.card_Ioi, Algebra.discr_powerBasis_eq_prod'', nonempty_Ioi, Algebra.discr_powerBasis_eq_prod', Fin.map_castSuccEmb_Ioi, WithTop.Ioc_coe_top, Fin.Ioi_sub_one_eq_Ici, IsMax.finsetIoi_eq, Ioo_subset_Ioi_self, Sum.Ioi_inl, Fin.Ioi_zero_eq_map, Fin.sum_Ioi_zero, Ici_add_one_eq_Ioi, Ioc_top, Fin.sum_Ioi_succ, Pi.card_Ioi, Fin.finsetImage_succ_Ioi, subtype_Ioi_eq, Ioi_mul_Ici_subset', Iio_ofDual, Ici_erase, Fin.map_castAddEmb_Ioi
|
Ioo 📖 | CompOp | 164 mathmath: Fin.map_succEmb_Iio, right_notMem_Ioo, prod_Ioo_mul_eq_prod_Ioc, Fin.Ico_add_one_eq_Ioo, Fin.finsetImage_castLE_Ioo, Ioo_map_sectR, Fin.finsetImage_castSucc_Ioo, left_notMem_Ioo, PNat.Ioo_eq_finset_subtype, Fin.finsetImage_val_Ioi, add_pow_prime_pow_eq, Fin.prod_Ioo_castLE, Sum.Lex.Ioo_inl_inr, Fin.attachFin_Ioo_eq_Ioi, Int.card_Ioo, Ioo_subset_Ici_self, Ioc_erase_right, Ioo_add_one_right_eq_Ioc_of_not_isMax, Fin.finsetImage_val_Ioo, LieModule.genWeightSpaceChain_def', Sum.Lex.Ioo_inr_inl, card_Ioo_finset, WithTop.Ioo_coe_top, tendsto_Ioo_atBot_prod_atTop, Ioo_subset_Icc_self, Set.toFinset_Ioo, image_add_left_Ioo, Sum.Lex.Ioo_inr_inr, Ioo_eq_filter_ssubsets, Fin.finsetImage_succ_Iio, Fin.map_finCongr_Ioo, mul_prod_Ioo_eq_prod_Ioc, Ioo_orderDual_def, Fin.prod_Ioo_castAdd, Fin.sum_Ioo_succ, sum_Ioo_add_eq_sum_Ico, WithTop.Ioo_coe_coe, Ioo_ofDual, Ico_add_one_left_eq_Ioo, Sum.Ioo_inl_inr, SummationFilter.symmetricIoo_filter, Fin.Ioo_add_one_eq_Ioc, Commute.add_pow_prime_pow_eq, Fintype.card_Ioo, Int.Ioo_eq_finset_map, nonempty_Ioo, Fin.sum_Ioo_castLE, tendsto_Ioo_neg, Ioc_eq_cons_Ioo, Fin.sum_Ioo_cast, card_Ioo_eq_card_Icc_sub_two, Fin.map_castLEEmb_Ioo, Ioc_diff_Ioo_self, Fin.prod_Ioo_cast, Finsupp.card_Ioo, Ioc_sub_one_right_eq_Ioo, Icc_succ_pred_eq_Ioo, coe_Ioo, Nat.card_Ioo, Ioo_succ_right_eq_Ioc, Ico_erase_left, Ioo_succ_right_eq_Ioc_of_not_isMax, DFinsupp.card_Ioo, Sum.Ioo_inr_inr, Ioo_toDual, sum_Ioo_inv_sq_le, Fin.finsetImage_castAdd_Ioi, Ioo_self, Ioc_mul_Ico_subset', PNat.map_subtype_embedding_Ioo, sum_Ioo_add_eq_sum_Ioc, Sum.Ioo_inr_inl, Fin.finsetImage_cast_Ioo, Sum.Lex.Ioo_inl_inl, Ioc_pred_right_eq_Ioo, mem_Ioo, Fin.card_Ioo, prod_Ioo_mul_eq_prod_Ico, filter_lt_lt_eq_Ioo, card_Ioo_eq_card_Ioc_sub_one, add_pow_prime_eq, Polynomial.Chebyshev.isLocalExtr_T_real_iff, map_add_left_Ioo, Sum.Ioo_inl_inl, Ioo_map_sectL, add_sum_Ioo_eq_sum_Ioc, Ioo_pred_left_eq_Ioc, Ioo_eq_empty_of_le, Fin.finsetImage_succ_Ioo, Fin.attachFin_Ioo, Fin.prod_Ioo_castSucc, Fin.map_revPerm_Ioo, Fin.finsetImage_castSucc_Ioi, Fin.map_valEmbedding_Ioi, Nat.smallSchroder_succ, mul_prod_Ioo_eq_prod_Ico, Fin.map_succEmb_Ioo, Ioo_insert_right, Fin.map_valEmbedding_Ioo, Ioo_subset_Ioo_right, Ioo_eq_empty_iff, Fin.sum_Ioo_castAdd, Icc_diff_both, Ico_add_Ioc_subset, Ioo_add_one_right_eq_Ioc, tendsto_Ioo_neg_atTop_atTop, map_add_right_Ioo, PNat.card_Ioo, Ioo_subset_Ioc_self, Ioo_subset_Ioo_left, Icc_subset_Ioo_iff, Icc_diff_Ioo_self, add_pow_prime_pow_eq', Ioo_filter_lt, card_Ioo_eq_card_Ico_sub_one, Ioo_sub_one_left_eq_Ioc, Ioo_eq_empty, Icc_add_one_sub_one_eq_Ioo, Ioo_succ_succ, Sigma.card_Ioo, add_pow_prime_eq', Ioo_subset_Iic_self, Fin.Ioo_sub_one_eq_Ico, Ioc_subset_Ioo_right, Ico_eq_cons_Ioo, Ioo_insert_left, Ico_diff_Ioo_self, Ioo_sub_one_left_eq_Ioc_of_not_isMin, Ioc_add_Ico_subset, Commute.add_pow_prime_eq, Fin.Ioc_sub_one_eq_Ioo, image_add_right_Ioo, WithBot.Ioo_coe_coe, Fin.finsetImage_addNat_Ioo, Ico_succ_left_eq_Ioo, Fin.map_castSuccEmb_Ioi, WithBot.Ioo_bot_coe, Ioo_subset_Ico_self, Fin.map_castSuccEmb_Ioo, Fin.finsetImage_natAdd_Ioo, Ico_subset_Ioo_left, Ioo_subset_Iio_self, Ioo_subset_Ioi_self, Ioo_pred_left_eq_Ioc_of_not_isMin, Commute.add_pow_prime_eq', Ioo_subset_Ioo, Fin.map_natAddEmb_Ioo, map_subtype_embedding_Ioo, Fin.map_addNatEmb_Ioo, Ico_mul_Ioc_subset', Fin.finsetImage_castAdd_Ioo, Fin.finsetImage_rev_Ioo, add_sum_Ioo_eq_sum_Ico, Fin.map_castAddEmb_Ioo, Multiset.card_Ioo, subtype_Ioo_eq, Sigma.Ioo_mk_mk, Fin.sum_Ioo_castSucc, Int.card_Ioo_of_lt, Commute.add_pow_prime_pow_eq', Pi.card_Ioo, Nat.Ioo_eq_range', Fin.prod_Ioo_succ, Fin.map_castAddEmb_Ioi
|
uIcc 📖 | CompOp | 77 mathmath: uIcc_of_le, Fin.prod_uIcc_cast, uIcc_toDual, Fin.finsetImage_castAdd_uIcc, uIcc_map_sectR, Icc_min_max, Fin.finsetImage_castSucc_uIcc, uIcc_eq_union, mem_uIcc', Fin.map_castLEEmb_uIcc, uIcc_of_ge, Icc_subset_uIcc', Fin.map_valEmbedding_uIcc, Fin.map_succEmb_uIcc, Fin.card_uIcc, mem_uIcc_of_le, uIcc_of_not_ge, Nat.uIcc_eq_range', Fin.map_natAddEmb_uIcc, right_mem_uIcc, uIcc_injective_right, uIcc_product_uIcc, uIcc_subset_uIcc_iff_le', uIcc_subset_uIcc_iff_le, Pi.card_uIcc, Fin.prod_uIcc_castLE, Multiset.card_uIcc, Fin.finsetImage_succ_uIcc, Finsupp.card_uIcc, Fin.map_finCongr_uIcc, PNat.uIcc_eq_finset_subtype, uIcc_comm, Fin.finsetImage_castLE_uIcc, Multiset.uIcc_eq, Fin.finsetImage_rev_uIcc, Fin.prod_uIcc_castSucc, uIcc_prod_def, Pi.uIcc_eq, uIcc_map_sectL, Fin.attachFin_uIcc, Int.card_uIcc, left_mem_uIcc, notMem_uIcc_of_gt, DFinsupp.card_uIcc, Int.uIcc_eq_finset_map, PNat.map_subtype_embedding_uIcc, uIcc_subset_uIcc_iff_mem, Fin.map_revPerm_uIcc, Icc_subset_uIcc, Fin.map_addNatEmb_uIcc, PNat.card_uIcc, Fin.sum_uIcc_castAdd, uIcc_subset_Icc, Fin.map_castAddEmb_uIcc, Fin.map_castSuccEmb_uIcc, Fin.sum_uIcc_castSucc, Fintype.card_uIcc, Fin.sum_uIcc_castLE, Fin.finsetImage_natAdd_uIcc, Fin.prod_uIcc_succ, Fin.finsetImage_val_uIcc, nonempty_uIcc, mem_uIcc_of_ge, Fin.prod_uIcc_castAdd, notMem_uIcc_of_lt, uIcc_self, card_uIcc_prod, uIcc_injective_left, Fin.finsetImage_cast_uIcc, uIcc_of_not_le, uIcc_subset_uIcc_union_uIcc, Fin.sum_uIcc_cast, Fin.finsetImage_addNat_uIcc, Nat.card_uIcc, coe_uIcc, mem_uIcc, Fin.sum_uIcc_succ
|