| Metric | Count |
|---|
Definitionsbliminf, blimsup, liminf, liminf_reparam, limsInf, limsSup, limsup, limsup_reparam | 8 |
Theoremsapply_liminf_iterate, apply_limsup_iterate, blimsup_eq_iInf_iSup, liminf_eq_ciSup_ciInf, liminf_eq_iSup_iInf, liminf_eq_ite, liminf_eq_sSup_iUnion_iInter, liminf_eq_sSup_univ_of_empty, limsInf_eq_iSup_sInf, limsSup_eq_iInf_sSup, limsup_eq_ciInf_ciSup, limsup_eq_iInf_iSup, limsup_eq_ite, limsup_eq_sInf_iUnion_iInter, limsup_eq_sInf_univ_of_empty, bliminf_antitone, bliminf_antitone_filter, bliminf_congr, bliminf_congr', bliminf_eq, bliminf_eq_iSup_biInf, bliminf_eq_iSup_biInf_of_nat, bliminf_eq_liminf, bliminf_eq_liminf_subtype, bliminf_false, bliminf_inf_not, bliminf_not_inf, bliminf_or_eq_inf, bliminf_or_le_inf, bliminf_or_le_inf_aux_left, bliminf_or_le_inf_aux_right, bliminf_sup_le_and, bliminf_sup_le_and_aux_left, bliminf_sup_le_and_aux_right, bliminf_sup_le_inf_aux_left, bliminf_sup_le_inf_aux_right, bliminf_sup_le_or_aux_left, bliminf_sup_le_or_aux_right, bliminf_true, blimsup_and_le_inf, blimsup_congr, blimsup_congr', blimsup_eq, blimsup_eq_iInf_biSup, blimsup_eq_iInf_biSup_of_nat, blimsup_eq_limsup, blimsup_eq_limsup_subtype, blimsup_false, blimsup_mono, blimsup_monotone_filter, blimsup_not_sup, blimsup_or_eq_sup, blimsup_sup_le_or, blimsup_sup_not, blimsup_true, bliminf_set_eq, blimsup_set_eq, liminf_set_eq, limsup_set_eq, eventually_add_neg_lt_of_le_liminf, eventually_lt_add_pos_of_limsup_le, eventually_lt_of_limsup_lt, eventually_lt_of_lt_liminf, exists_forall_mem_of_hasBasis_mem_blimsup, exists_forall_mem_of_hasBasis_mem_blimsup', exists_lt_of_le_liminf, exists_lt_of_limsup_le, frequently_lt_of_liminf_lt, frequently_lt_of_limsInf_lt, frequently_lt_of_lt_limsSup, frequently_lt_of_lt_limsup, gt_mem_sets_of_limsInf_gt, iInf_le_liminf, inf_liminf, inf_limsup, le_liminf_iff, le_liminf_iff', le_liminf_of_le, le_limsInf_of_le, le_limsSup_of_le, le_limsup_iff, le_limsup_iff', le_limsup_of_frequently_le, le_limsup_of_frequently_le', le_limsup_of_le, liminf_bot, liminf_comp, liminf_compl, liminf_congr, liminf_const, liminf_const_top, liminf_eq, liminf_eq_iSup_iInf, liminf_eq_iSup_iInf_of_nat, liminf_eq_iSup_iInf_of_nat', liminf_eq_sSup_sInf, liminf_le_iff, liminf_le_iff', liminf_le_liminf, liminf_le_liminf_of_le, liminf_le_limsup, liminf_le_limsup_of_frequently_le, liminf_le_of_frequently_le, liminf_le_of_frequently_le', liminf_le_of_le, liminf_nat_add, liminf_piecewise, liminf_sdiff, liminf_sup_filter, liminf_top_eq_ciInf, liminf_top_eq_iInf, limsInf_bot, limsInf_eq_iSup_sInf, limsInf_le_limsInf, limsInf_le_limsInf_of_le, limsInf_le_limsSup, limsInf_le_of_le, limsInf_principal_eq_csSup, limsInf_principal_eq_sInf, limsInf_top, limsSup_bot, limsSup_eq_iInf_sSup, limsSup_le_limsSup, limsSup_le_limsSup_of_le, limsSup_le_of_le, limsSup_principal_eq_csSup, limsSup_principal_eq_sSup, limsSup_top, limsup_bot, limsup_comp, limsup_compl, limsup_congr, limsup_const, limsup_const_bot, limsup_eq, limsup_eq_iInf_iSup, limsup_eq_iInf_iSup_of_nat, limsup_eq_iInf_iSup_of_nat', limsup_eq_sInf_sSup, limsup_le_iSup, limsup_le_iff, limsup_le_iff', limsup_le_limsup, limsup_le_limsup_of_le, limsup_le_of_le, limsup_nat_add, limsup_piecewise, limsup_sdiff, limsup_sup_filter, limsup_top_eq_ciSup, limsup_top_eq_iSup, lt_mem_sets_of_limsSup_lt, mem_liminf_iff_eventually_mem, mem_limsup_iff_frequently_mem, mono_bliminf, mono_bliminf', mono_blimsup, mono_blimsup', sdiff_liminf, sdiff_limsup, sup_liminf, sup_limsup, l_limsup_le, apply_bliminf, apply_blimsup, liminf_apply, limsup_apply, liminf_finset_inf, liminf_finset_inf', liminf_min, limsup_finset_sup, limsup_finset_sup', limsup_max, le_apply_bliminf, apply_blimsup_le | 175 |
| Total | 183 |
| Name | Category | Theorems |
|---|
bliminf 📖 | CompOp | 27 mathmath: sInfHom.le_apply_bliminf, bliminf_congr', bliminf_sup_le_and_aux_right, bliminf_inf_not, bliminf_sup_le_and_aux_left, bliminf_sup_le_and, bliminf_antitone, bliminf_true, bliminf_eq_iSup_biInf_of_nat, mono_bliminf, bliminf_or_le_inf, bliminf_or_eq_inf, cofinite.bliminf_set_eq, MeasurableSet.measurableSet_bliminf, bliminf_eq, mono_bliminf', bliminf_or_le_inf_aux_left, bliminf_congr, bliminf_antitone_filter, bliminf_not_inf, bliminf_or_le_inf_aux_right, bliminf_eq_liminf_subtype, bliminf_eq_iSup_biInf, bliminf_false, liminf_piecewise, OrderIso.apply_bliminf, bliminf_eq_liminf
|
blimsup 📖 | CompOp | 36 mathmath: bliminf_sup_le_or_aux_right, blimsup_and_le_inf, blimsup_eq_limsup, blimsup_true, blimsup_eq, blimsup_thickening_mul_ae_eq_aux, bliminf_sup_le_or_aux_left, blimsup_cthickening_ae_le_of_eventually_mul_le_aux, blimsup_cthickening_ae_le_of_eventually_mul_le, blimsup_eq_iInf_biSup, blimsup_sup_not, bliminf_sup_le_inf_aux_left, bliminf_sup_le_inf_aux_right, mem_add_wellApproximable_iff, blimsup_congr', mem_wellApproximable_iff, blimsup_eq_limsup_subtype, mono_blimsup, MeasurableSet.measurableSet_blimsup, HasBasis.blimsup_eq_iInf_iSup, blimsup_cthickening_ae_eq_blimsup_thickening, cofinite.blimsup_set_eq, blimsup_mono, limsup_piecewise, OrderIso.apply_blimsup, blimsup_thickening_mul_ae_eq, blimsup_sup_le_or, blimsup_not_sup, blimsup_eq_iInf_biSup_of_nat, blimsup_cthickening_mul_ae_eq, blimsup_false, blimsup_or_eq_sup, blimsup_monotone_filter, blimsup_congr, mono_blimsup', sSupHom.apply_blimsup_le
|
liminf 📖 | CompOp | 133 mathmath: liminf_const_sub, liminf_eq, HasBasis.liminf_eq_ite, sdiff_limsup, Antitone.map_limsup_of_continuousAt, ENNReal.le_liminf_mul, liminf_comp, MeasureTheory.liminf_ae_eq_of_forall_ae_eq, bliminf_inf_not, liminf_const_top, LowerSemicontinuousOn.le_liminf, MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top, le_limsup_add, MeasureTheory.measure_liminf_cofinite_eq_zero, liminf_eq_iSup_iInf_of_nat', ENNReal.limsup_liminf_le_liminf_limsup, limsup_compl, MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum, spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div, bliminf_true, ENNReal.liminf_toReal_eq, Antitone.map_limsSup_of_continuousAt, lowerSemicontinuous_iff_le_liminf, MeasureTheory.Measure.QuasiMeasurePreserving.liminf_preimage_iterate_ae_eq, MeasureTheory.Measure.mkMetric_le_liminf_tsum, Real.liminf_of_not_isBoundedUnder, liminf_eq_top, EReal.limsup_neg, liminf_le_iff', LowerSemicontinuousWithinAt.le_liminf, LowerSemicontinuousAt.le_liminf, liminf_add_le, liminf_le_of_frequently_le', ENNReal.liminf_sub_const, MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge, liminf_add_const, MeasureTheory.lintegral_liminf_le, liminf_sup_filter, liminf_eq_sSup_sInf, CompleteLatticeHom.apply_liminf_iterate, liminf_sub_const, ENNReal.liminf_mul_le, EReal.le_liminf_add, OrderIso.liminf_apply, MeasureTheory.le_liminf_measure_open_of_forall_tendsto_measure, EReal.liminf_add_le, ENNReal.liminf_const_sub, liminf_const, MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm, MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto, le_limsup_mul, Real.liminf_of_not_isCoboundedUnder, liminf_congr, MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd, ENNReal.essSup_liminf_le, liminf_compl, liminf_le_of_frequently_le, LowerSemicontinuous.le_liminf, HasBasis.liminf_eq_iSup_iInf, MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf, liminf_sdiff, le_liminf_iff', eventually_liminf_le, EReal.le_limsup_mul, ENNReal.ofNNReal_liminf, EReal.le_liminf_mul, liminf_eq_iSup_iInf_of_nat, Measurable.liminf', MeasureTheory.measure_liminf_atTop_eq_zero, HasBasis.liminf_eq_sSup_univ_of_empty, MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum, Tendsto.liminf_eq, MeasurableSet.measurableSet_liminf, EReal.liminf_neg, cofinite.liminf_set_eq, EReal.liminf_mul_le, lowerSemicontinuousWithinAt_iff_le_liminf, Monotone.map_limsInf_of_continuousAt, Measurable.liminf, liminf_le_limsup_of_frequently_le, liminf_mul_le, lowerSemicontinuousAt_iff_le_liminf, liminf_le_iff, liminf_le_limsup, liminf_eq_iSup_iInf, HasBasis.liminf_eq_sSup_iUnion_iInter, inf_liminf, MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd, ENNReal.liminf_add_of_right_tendsto_zero, liminf_finset_inf', MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, liminf_le_liminf, ENNReal.tsum_eq_liminf_sum_nat, EReal.le_limsup_add, liminf_nat_add, iInf_le_liminf, liminf_bot, MeasureTheory.le_measure_compl_liminf_of_limsup_measure_le, MeasureTheory.Measure.mkMetric_le_liminf_sum, MeasureTheory.lintegral_enorm_le_liminf_of_tendsto, NNReal.liminf_of_not_isCoboundedUnder, MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf, bliminf_not_inf, sdiff_liminf, le_liminf_add, le_liminf_mul, liminf_top_eq_iInf, ENNReal.liminf_add_of_left_tendsto_zero, liminf_finset_inf, liminf_top_eq_ciInf, ENNReal.limsup_const_sub, ENNReal.le_limsup_mul, bliminf_eq_liminf_subtype, MeasureTheory.lintegral_liminf_le', ENNReal.inv_liminf, ENNReal.inv_limsup, NNReal.toReal_liminf, liminf_le_of_le, liminf_piecewise, le_liminf_iff, sup_liminf, FormalMultilinearSeries.radius_eq_liminf, liminf_min, liminf_le_liminf_of_le, HasBasis.liminf_eq_ciSup_ciInf, lowerSemicontinuousOn_iff_le_liminf, limsup_const_sub, MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm', mem_liminf_iff_eventually_mem, le_liminf_of_le, MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le, bliminf_eq_liminf, liminf_const_add
|
liminf_reparam 📖 | CompOp | 2 mathmath: HasBasis.liminf_eq_ite, HasBasis.liminf_eq_ciSup_ciInf
|
limsInf 📖 | CompOp | 17 mathmath: limsInf_le_limsSup, NNReal.limsInf_of_not_isCobounded, limsInf_le_limsInf_of_le, SummationFilter.support_eq_limsInf, limsInf_eq_of_le_nhds, HasBasis.limsInf_eq_iSup_sInf, le_limsInf_of_le, limsInf_le_limsInf, limsInf_top, limsInf_le_of_le, Real.limsInf_of_not_isBounded, Real.limsInf_of_not_isCobounded, limsInf_bot, limsInf_nhds, limsInf_principal_eq_sInf, limsInf_eq_iSup_sInf, limsInf_principal_eq_csSup
|
limsSup 📖 | CompOp | 16 mathmath: limsInf_le_limsSup, le_limsSup_of_le, Real.limsSup_of_not_isCobounded, limsSup_le_limsSup, limsSup_eq_of_le_nhds, limsSup_eq_iInf_sSup, limsSup_principal_eq_csSup, limsSup_bot, NNReal.limsSup_of_not_isBounded, limsSup_le_of_le, limsSup_principal_eq_sSup, HasBasis.limsSup_eq_iInf_sSup, Real.limsSup_of_not_isBounded, limsSup_le_limsSup_of_le, limsSup_top, limsSup_nhds
|
limsup 📖 | CompOp | 152 mathmath: Measurable.limsup, Tendsto.limsup_eq, liminf_const_sub, limsup_comp, limsup_nat_add, ProbabilityTheory.measure_limsup_eq_one, sdiff_limsup, ENNReal.ofNNReal_limsup, le_limsup_of_frequently_le, limsup_const, CompleteLatticeHom.apply_limsup_iterate, ENNReal.limsup_const_mul_of_ne_top, ProbabilityTheory.Kernel.indep_iSup_directed_limsup, Real.limsup_of_not_isBoundedUnder, ProbabilityTheory.indep_limsup_atTop_self, le_limsup_add, OrderIso.limsup_apply, ENNReal.limsup_mul_le, blimsup_eq_limsup, ENNReal.limsup_const_mul, ENNReal.limsup_liminf_le_liminf_limsup, limsup_compl, blimsup_true, ProbabilityTheory.Kernel.indep_limsup_atBot_self, limsup_top_eq_ciSup, MeasureTheory.limsup_lintegral_le, HasBasis.limsup_eq_sInf_univ_of_empty, inf_limsup, ProbabilityTheory.indep_biSup_limsup, HasBasis.limsup_eq_ite, ProbabilityTheory.Kernel.indep_iSup_limsup, HasBasis.limsup_eq_sInf_iUnion_iInter, cofinite.limsup_set_eq, le_limsup_of_frequently_le', ProbabilityTheory.condIndep_limsup_atTop_self, EReal.limsup_neg, ProbabilityTheory.Kernel.indep_limsup_self, ENNReal.ofReal_limsup, limsup_const_add, limsup_eq_bot, MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure, limsup_sup_filter, liminf_add_le, MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge, le_limsup_iff, upperSemicontinuousWithinAt_iff_limsup_le, UpperSemicontinuousWithinAt.limsup_le, limsup_sdiff, MeasureTheory.limsup_measure_compl_le_of_le_liminf_measure, upperSemicontinuousOn_iff_limsup_le, MeasureTheory.measure_limsup_cofinite_eq_zero, ENNReal.liminf_mul_le, FormalMultilinearSeries.radius_inv_eq_limsup, blimsup_sup_not, EReal.liminf_add_le, ProbabilityTheory.indep_iSup_limsup, limsup_le_iff, Measurable.limsup', ENNReal.liminf_const_sub, MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto, le_limsup_of_le, limsup_le_of_le, le_limsup_mul, Real.limsup_of_not_isCoboundedUnder, le_limsup_iff', MeasureTheory.limsup_trim, UpperSemicontinuousOn.limsup_le, ProbabilityTheory.condIndep_iSup_limsup, Set.limsup_eq_tendsto_sum_indicator_atTop, sup_limsup, liminf_compl, Antitone.map_liminf_of_continuousAt, limsup_le_iff', ProbabilityTheory.indep_iSup_directed_limsup, ENNReal.tsum_eq_limsup_sum_nat, UpperSemicontinuousAt.limsup_le, EReal.le_limsup_mul, ENNReal.toReal_limsup, EReal.limsup_mul_le, spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius, ProbabilityTheory.condIndep_biSup_limsup, upperSemicontinuousAt_iff_limsup_le, ProbabilityTheory.condIndep_limsup_self, eventually_le_limsup, limsup_bot, upperSemicontinuous_iff_limsup_le, ProbabilityTheory.Kernel.indep_biSup_limsup, ProbabilityTheory.indep_limsup_atBot_self, EReal.liminf_neg, Monotone.map_limsSup_of_continuousAt, ENNReal.limsup_eq_zero_iff, EReal.liminf_mul_le, liminf_le_limsup_of_frequently_le, blimsup_eq_limsup_subtype, liminf_mul_le, ENNReal.limsup_add_of_right_tendsto_zero, ProbabilityTheory.condIndep_iSup_directed_limsup, liminf_le_limsup, ProbabilityTheory.Kernel.indep_limsup_atTop_self, MeasurableSet.measurableSet_limsup, limsup_max, ENNReal.limsup_mul_le', MeasureTheory.ae_mem_limsup_atTop_iff, GaloisConnection.l_limsup_le, mem_limsup_iff_frequently_mem, limsup_add_le, MeasureTheory.measure_limsup_atTop_eq_zero, NNReal.limsup_of_not_isBoundedUnder, limsup_eq_iInf_iSup, limsup_le_iSup, limsup_const_bot, EReal.le_limsup_add, limsup_le_limsup, MeasureTheory.limsup_ae_eq_of_forall_ae_eq, limsup_eq_iInf_iSup_of_nat', sdiff_liminf, limsup_finset_sup, NNReal.toReal_limsup, limsup_piecewise, blimsup_not_sup, limsup_congr, ProbabilityTheory.condIndep_limsup_atBot_self, limsup_eq_sInf_sSup, MeasureTheory.limsup_measure_le_of_le_liminf_measure_compl, limsup_eq_iInf_iSup_of_nat, bsupr_limsup_dimH, ENNReal.limsup_const_sub, limsup_eq, ENNReal.le_limsup_mul, ENNReal.limsup_add_le, ENNReal.limsup_sub_const, ENNReal.inv_liminf, limsup_finset_sup', ENNReal.eventually_le_limsup, ENNReal.inv_limsup, HasBasis.limsup_eq_iInf_iSup, ENNReal.limsup_toReal_eq, HasBasis.limsup_eq_ciInf_ciSup, limsup_sub_const, ENNReal.limsup_add_of_left_tendsto_zero, limsup_le_limsup_of_le, limsup_mul_le, MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto, limsup_const_sub, MeasureTheory.Measure.QuasiMeasurePreserving.limsup_preimage_iterate_ae_eq, limsup_add_const, iSup_limsup_dimH, UpperSemicontinuous.limsup_le, ProbabilityTheory.indep_limsup_self, EReal.limsup_add_le, Antitone.map_limsInf_of_continuousAt, limsup_top_eq_iSup
|
limsup_reparam 📖 | CompOp | 2 mathmath: HasBasis.limsup_eq_ite, HasBasis.limsup_eq_ciInf_ciSup
|