| Name | Category | Theorems |
|---|
ceil 📖 | CompOp | 111 mathmath: ceil_lt_iff, continuousOn_ceil, ceil_eq_self_iff_mem, lt_ceil, tendsto_ceil_right', ceil_div_ceil_inv_sub_one, ceil_neg, Rat.ceil_intCast_div_natCast, ceil_one_add, tendsto_ceil_left_pure_ceil, tendsto_ceil_atTop, ceil_sub_intCast, ceil_lt_two_mul, le_ceil, ceil_ofNat, Rat.isNat_intCeil_ofIsNNRat, CircleDeg1Lift.map_le_of_map_zero, Polynomial.card_eq_of_natDegree_le_of_coeff_le, ceil_int, tendsto_ceil_right_pure_add_one, ceil_eq_iff, ceil_sub_natCast, preimage_Iio, ZSpan.repr_ceil_apply, ceil_eq_zero_iff, Measurable.ceil, map_ceil, Rat.isNat_intCeil, ball_eq_Ioo, floor_neg, NNRat.intCeil_cast, ceil_eq_on_Ioc', ceil_intCast, ceil_add_one, tendsto_ceil_right_pure_floor_add_one, natCast_ceil_eq_intCast_ceil_of_neg_one_lt, tendsto_ceil_left, tendsto_ceil_atBot, NNRat.coe_ceil, Rat.isInt_intCeil, ceil_nonneg, Rat.ceil_natCast_div_natCast, ceil_add_natCast, ceil_eq_floor_add_one_iff_notMem, ceil_sub_one, le_ceil_iff, Nat.Ico_filter_modEq_card, Ico_filter_dvd_card, CircleDeg1Lift.translationNumber_le_ceil_sub, Rat.den_le_and_le_num_le_of_sub_lt_one_div_den_sq, tendsto_ceil_left_pure, ceil_zero, Real.ceil_exp_one_eq_three, floor_le_ceil, ceil_le_two_mul, ceil_eq_add_one_sub_fract, natCast_ceil_eq_intCast_ceil, CircleDeg1Lift.le_ceil_map_map_zero, Real.ceil_pi_eq_four, BoxIntegral.unitPartition.index_apply, one_le_ceil_iff, ceil_nonneg_of_neg_one_lt, ceil_le, ceil_lt_add_one, preimage_Ioo, tendsto_ceil_left', Real.ceil_logb_natCast, ceil_toNat, preimage_Ici, closedBall_eq_Icc, Ico_filter_modEq_card, preimage_Icc, ceil_sub_self_eq, natCast_ceil_eq_ceil, CircleDeg1Lift.ceil_map_map_zero_le, ceil_pos, round_eq_half_ceil_two_mul, Rat.ceil_cast, tendsto_floor_left_pure_ceil_sub_one, measurable_ceil, ceil_add_ofNat, gc_ceil_coe, ceil_eq_on_Ioc, ceil_le_floor_add_one, Mathlib.Meta.Positivity.int_ceil_pos, ceil_sub_ofNat, fract_eq_zero_or_add_one_sub_ceil, ceil_congr, floorRing_ceil_eq, preimage_ceil_singleton, ceil_mono, tendsto_ceil_right, ceil_add_intCast, Nat.count_modEq_card_eq_ceil, ceil_le_ceil, natCast_ceil_eq_ceil_of_neg_one_lt, CircleDeg1Lift.floor_map_map_zero_le, ceil_add_le, ceil_ofNat_add, CircleDeg1Lift.map_map_zero_le, Ico_filter_dvd_eq, add_one_le_ceil_iff, preimage_Ico, ceil_add_ceil_le, ceil_natCast_add, ceil_one, Rat.ceil_def', ceil_natCast, ceil_intCast_add, Rat.isInt_intCeil_ofIsRat_neg, floor_lt_ceil_of_lt
|
floor 📖 | CompOp | 146 mathmath: Rat.num_lt_succ_floor_mul_den, mul_cast_floor_div_cancel_of_pos, NNRat.coe_floor, lt_succ_floor, floor_nonpos, floor_one, floor_int, preimage_Ioc, continuousOn_floor, floor_add_one, ceil_neg, floor_sub_one, Rat.isInt_intFloor, round_eq_div, CircleDeg1Lift.map_lt_add_floor_translationNumber_add_one, floor_intCast, tendsto_floor_right_pure, preimage_Ioi, floor_eq_zero_iff, fract_floor, floor_intCast_add, CircleDeg1Lift.floor_sub_le_translationNumber, Function.Periodic.sInf_add_zsmul_le_integral_of_pos, GenContFract.compExactValue_correctness_of_stream_eq_some_aux_comp, floor_natCast, GenContFract.convs'_succ, CircleDeg1Lift.le_map_of_map_zero, floor_lt, floor_div_natCast, Polynomial.card_eq_of_natDegree_le_of_coeff_le, Rat.floor_natCast_div_natCast, Complex.arg_cos_add_sin_mul_I_sub, floor_add_ofNat, tendsto_floor_right_pure_floor, floor_le_iff, floor_le_sub_one_iff, floor_eq_on_Ico', floor_nonneg, floor_div_cast_of_nonneg, CircleDeg1Lift.le_floor_map_map_zero, tendsto_floor_atTop, natCast_floor_eq_intCast_floor, floor_mono, ball_eq_Ioo, floor_sub_ofNat, floor_neg, lt_floor_add_one, natCast_floor_eq_floor, Rat.floor_cast, floor_congr, sub_one_lt_floor, Real.convergent_succ, tendsto_ceil_right_pure_floor_add_one, fract_div_mul_self_add_zsmul_eq, cast_mul_floor_div_cancel_of_pos, floor_add_fract, toIcoDiv_zero_one, Nat.Ioc_filter_modEq_card, Ioc_filter_modEq_card, natCast_mul_floor_div_cancel, ceil_eq_floor_add_one_iff_notMem, tendsto_floor_right, Real.floor_real_sqrt_eq_nat_sqrt, Real.convergent_zero, ZSpan.coe_floor_self, measurable_floor, gc_coe_floor, CircleDeg1Lift.le_map_map_zero, GenContFract.convs_succ, floor_eq_self_iff_mem, preimage_Iic, round_eq, floor_zero, Rat.isNat_intFloor, floor_eq_iff, Rat.den_le_and_le_num_le_of_sub_lt_one_div_den_sq, Mathlib.Meta.Positivity.int_floor_nonneg_of_pos, fract_sub_self, tendsto_floor_left', GenContFract.of_s_head, floor_le_ceil, floor_fract, Nat.coprime_sub_mul_floor_rat_div_of_coprime, self_sub_floor, toIocDiv_eq_neg_floor, map_floor, floor_natCast_add, CircleDeg1Lift.le_ceil_map_map_zero, floor_toNat, floor_add_natCast, self_sub_fract, sub_floor_div_mul_nonneg, Mathlib.Meta.Positivity.int_floor_nonneg, Rat.floor_def', tendsto_floor_atBot, mul_lt_floor, preimage_Ioo, Rat.isNat_intFloor_ofIsNNRat, floor_le_neg_one_iff, floor_ofNat_add, floor_add_intCast, floor_pos, closedBall_eq_Icc, le_floor_add_floor, le_floor, Ioc_filter_dvd_eq, preimage_Icc, Real.floor_logb_natCast, Real.floor_pi_eq_three, preimage_floor_singleton, tendsto_floor_left_pure_ceil_sub_one, floor_lt_self_iff, toIcoDiv_eq_floor, floor_le, ceil_le_floor_add_one, fract_add_floor, Measurable.floor, floor_sub_natCast, Function.Periodic.integral_le_sSup_add_zsmul_of_pos, GenContFract.of_h_eq_floor, floor_le_floor, tendsto_floor_left, Real.floor_exp_one_eq_two, GenContFract.IntFractPair.exists_succ_nth_stream_of_fr_zero, mul_natCast_floor_div_cancel, div_two_lt_floor, CircleDeg1Lift.floor_map_map_zero_le, ZSpan.repr_floor_apply, floorRing_floor_eq, Complex.arg_mul_cos_add_sin_mul_I_sub, tendsto_floor_left_pure_sub_one, NNRat.intFloor_cast, CircleDeg1Lift.mul_floor_map_zero_le_floor_iterate_zero, tendsto_floor_right', lt_floor_iff, floor_eq_on_Ico, mod_nat_eq_sub_mul_floor_rat_div, Rat.floor_intCast_div_natCast, le_floor_add, floor_ofNat, Rat.isInt_intFloor_ofIsRat_neg, AddConstMapClass.map_fract, sub_floor_div_mul_lt, Ioc_filter_dvd_card, floor_sub_intCast, floor_lt_ceil_of_lt
|
fract 📖 | CompOp | 93 mathmath: fract_intCast_add, AddCircle.coe_equivIco_mk_apply, map_fract, toIcoMod_eq_fract_mul, Rat.isNat_intFract_of_isNat, fract_add_one, fract_add_ofNat, fract_div_mul_self_mem_Ico, fract_add_fract_le, Measurable.fract, Rat.cast_fract, tendsto_fract_left', MeasurableSet.image_fract, continuousOn_fract, fract_floor, GenContFract.compExactValue_correctness_of_stream_eq_some_aux_comp, fract_pos, GenContFract.convs'_succ, fract_one_add, fract_sub_one, fract_intCast, tendsto_fract_right', measurable_fract, fract_natCast, fract_eq_fract, Real.convergent_succ, fract_div_mul_self_add_zsmul_eq, AddCircle.coe_fract, toIcoMod_eq_add_fract_mul, toIocMod_eq_sub_fract_mul, fract_add_natCast, abs_sub_round_eq_min, fract_int, floor_add_fract, fract_sub_natCast, fract_one, fract_periodic, abs_fract, unitInterval.fract_mem, ContinuousOn.comp_fract', Rat.isNat_intFract_of_isInt, GenContFract.convs_succ, continuousAt_fract, Rat.fract_inv_num_lt_num_of_pos, fract_sub_self, GenContFract.of_s_head, fract_add, fract_neg, floor_fract, ceil_eq_add_one_sub_fract, self_sub_floor, fract_natCast_add, self_sub_fract, fract_add_le, image_fract, Rat.isRat_intFract_of_isRat_negOfNat, fract_add_intCast, fract_eq_zero_iff, fract_sub_intCast, GenContFract.of_s_tail, tendsto_fract_left, fract_div_natCast_eq_div_natCast_mod, fract_fract, fract_neg_eq_zero, fract_ofNat, ZSpan.repr_fract_apply, fract_eq_self, fract_lt_one, ceil_sub_self_eq, abs_one_sub_fract, toIcoMod_zero_one, fract_add_floor, fract_eq_zero_or_add_one_sub_ceil, mul_fract_eq_one_iff_exists_int, ContinuousOn.comp_fract, CircleDeg1Lift.map_fract_sub_fract_eq, Rat.isNNRat_intFract_of_isNNRat, fract_nonneg, preimage_fract, fract_ofNat_add, tendsto_fract_right, ZSpan.coe_fract_self, Rat.den_intFract, fract_mul_natCast, fract_zero, fract_sub_ofNat, AddConstMapClass.map_fract, ContinuousOn.comp_fract'', GenContFract.of_s_succ, fract_div_intCast_eq_div_intCast_mod, GenContFract.IntFractPair.stream_succ, niven_fract_angle_div_pi_eq, fract_eq_iff
|
«term⌈_⌉» 📖 | CompOp | — |
«term⌊_⌋» 📖 | CompOp | — |
| Name | Category | Theorems |
|---|
ceil 📖 | CompOp | 71 mathmath: ceil_pos, preimage_Iio, ceil_int, preimage_Ici, ceil_le_two_mul, ceil_eq_zero, ceil_lt_two_mul, preimage_Icc, ceil_lt_add_one_of_gt_neg_one, closedBall_eq_Icc, SimpleGraph.triangleRemovalBound_mul_cube_lt, ceil_mono, preimage_Ioo, ceil_le_ceil, Asymptotics.isEquivalent_nat_ceil, measurable_ceil, ceil_lt_add_one, Mathlib.Meta.NormNum.IsNat.natCeil, Real.natCeil_logb_natCast, natCast_ceil_eq_intCast_ceil_of_neg_one_lt, Mathlib.Meta.Positivity.nat_ceil_pos, preimage_ceil_of_ne_zero, NNRat.coe_ceil, ceil_add_one, Behrend.exp_neg_two_mul_le, ceil_le_floor_add_one, tendsto_nat_ceil_atTop, abs_sub_ceil_le, map_ceil, ceil_intCast, gc_ceil_coe, ceil_one, Behrend.ceil_lt_mul, ceil_ofNat, ceil_sub_natCast, ceil_add_natCast, ceil_nat, Int.clog_of_one_le_right, NNRat.ceil_coe, natCast_ceil_eq_intCast_ceil, ceil_add_ofNat, floor_le_ceil, tendsto_nat_ceil_div_atTop, Mathlib.Meta.NormNum.IsRat.natCeil, Int.ceil_toNat, NNRat.ceil_cast, ceil_sub_ofNat, ceil_sub_one, Int.natCast_ceil_eq_ceil, SimpleGraph.triangleRemovalBound_le, one_le_ceil_iff, tendsto_nat_ceil_mul_div_atTop, lt_ceil, Nonneg.nat_ceil_coe, le_ceil, ceil_zero, ceil_natCast, Mathlib.Meta.NormNum.IsInt.natCeil, ENat.ceil_coe, Int.log_of_right_le_one, Int.natCast_ceil_eq_ceil_of_neg_one_lt, ceil_congr, ceil_eq_iff, add_one_le_ceil_iff, Measurable.nat_ceil, floor_lt_ceil_of_lt_of_pos, abs_ceil_sub_le, ceil_le, preimage_Ico, preimage_ceil_zero, ceil_add_le
|
floor 📖 | CompOp | 121 mathmath: NNRat.coe_floor, Mathlib.Meta.NormNum.IsNNRat.natFloor, floor_add_one, Chebyshev.theta_eq_theta_coe_floor, Real.natFloor_logb_natCast, floor_eq_iff, Real.nat_floor_real_sqrt_eq_nat_sqrt, tendsto_smul_comp_nat_floor_of_tendsto_mul, floor_div_natCast, preimage_Ioi, tendsto_nat_floor_mul_atTop, measurable_floor, NNRat.floor_coe, Chebyshev.psi_eq_psi_coe_floor, lt_succ_floor, floor_sub_one, Chebyshev.psi_eq_sum_theta, floor_add_natCast, Chebyshev.psi_sub_theta_eq_sum_not_prime, map_floor, preimage_Ioc, floor_div_ofNat, preimage_Icc, closedBall_eq_Icc, NNRat.floor_cast, floor_le_of_le, le_floor_iff', preimage_Ioo, Int.clog_of_right_le_one, preimage_floor_of_ne_zero, floor_eq_on_Ico', floor_le_floor, sum_mul_eq_sub_integral_mul', floor_natCast, one_le_floor_iff, LSeries_eq_mul_integral_of_nonneg, Chebyshev.sum_PrimePow_eq_sum_sum, natCast_floor_eq_intCast_floor, floor_int, Int.natCast_floor_eq_floor, Chebyshev.primeCounting_eq_theta_div_log_add_integral, sum_div_nat_floor_pow_sq_le_div_sq, tendsto_nat_floor_mul_div_atTop, floor_div_eq_div, floor_lt', preimage_Iic, le_floor_iff, floor_lt_one, tendsto_nat_floor_div_atTop, floor_le_one_of_le_one, Chebyshev.primeCounting_sub_theta_div_log_isBigO, floor_lt, ceil_le_floor_add_one, sum_mul_eq_sub_integral_mul₀', Mathlib.Meta.NormNum.IsRat.natFloor, ENat.floor_coe, floor_ofNat, Chebyshev.theta_eq_log_primorial, ProbabilityTheory.strong_law_aux6, Rat.natFloor_natCast_div_natCast, div_two_lt_floor, harmonic_floor_le_one_add_log, floor_nat, abs_sub_floor_le, sum_mul_eq_sub_integral_mul₁, Chebyshev.psi_eq_theta_add_sum_theta, tendsto_nat_floor_atTop, LSeries_eq_mul_integral, floor_of_nonpos, Asymptotics.isEquivalent_nat_floor, Int.floor_toNat, floor_le_ceil, floor_congr, Chebyshev.theta_eq_sum_Icc, log_le_harmonic_floor, Int.log_of_one_le_right, Measurable.nat_floor, abs_floor_sub_le, floor_add_ofNat, locallyIntegrableOn_mul_sum_Icc, floor_sub_natCast, ProbabilityTheory.strong_law_aux4, Chebyshev.psi_eq_sum_Icc, integrableOn_mul_sum_Icc, Int.abs_le_floor_nnreal_iff, floor_le, preimage_floor_zero, floor_eq_zero, le_floor, ProbabilityTheory.strong_law_aux1, sub_one_lt_floor, floor_mono, NNRat.floor_def, ProbabilityTheory.strong_law_aux2, Behrend.div_lt_floor, Mathlib.Meta.NormNum.IsInt.natFloor, sum_mul_eq_sub_sub_integral_mul', floor_zero, Nonneg.nat_floor_coe, floor_one, floor_sub_ofNat, sum_mul_eq_sub_integral_mul, floor_eq_iff', NNRat.floor_natCast_div_natCast, Complex.Gamma_def, cast_mul_floor_div_cancel, mul_cast_floor_div_cancel, sum_mul_eq_sub_integral_mul₀, sum_mul_eq_sub_sub_integral_mul, floor_lt_ceil_of_lt_of_pos, Chebyshev.eventually_primeCounting_le, Mathlib.Meta.NormNum.IsNat.natFloor, lt_floor_add_one, mul_lt_floor, LSeries_eq_mul_integral', mul_pow_le_nat_floor_pow, Polynomial.card_mahlerMeasure_le_prod, floor_eq_on_Ico, Real.ofDigits_digits_sum_eq, tendsto_smul_comp_nat_floor_of_tendsto_nsmul, floor_pos
|
«term⌈_⌉₊» 📖 | CompOp | — |
«term⌊_⌋₊» 📖 | CompOp | — |