Leibniz

📁 Source: Mathlib/Analysis/Real/Pi/Leibniz.lean

Statistics

Metric	Count
Definitions	0
Theorems tendsto_sum_pi_div_four	1
Total	1

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_sum_pi_div_four 📖	mathematical	—	Filter.Tendsto Real Finset.sum instAddCommMonoid Finset.range DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instNeg instOne instAdd instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace pi	—	Nat.instAtLeastTwoHAddOfNat Antitone.tendsto_alternating_series_of_tendsto_zero antitone_iff_forall_lt inv_anti₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing le_of_lt Mathlib.Meta.Positivity.pos_of_isNat instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_nonneg' instZeroLEOneClass Nat.cast_one add_le_add_left mul_le_mul_of_nonneg_left Nat.mono_cast Filter.Tendsto.inv_tendsto_atTop instOrderTopologyReal Filter.tendsto_atTop_add_const_right Filter.Tendsto.const_mul_atTop zero_lt_two NeZero.charZero_one RCLike.charZero_rclike tendsto_natCast_atTop_atTop instArchimedean tendsto_tsum_powerSeries_nhdsWithin_lt tendsto_nhdsWithin_of_tendsto_nhds tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within one_pow Filter.Tendsto.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.eventually_iff_exists_mem Ioo_mem_nhdsLT instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Set.mem_Iio sq_lt_one_iff_abs_lt_one abs_lt Set.mem_Ioo Filter.Tendsto.mul Filter.Tendsto.comp Filter.Tendsto.congr' mul_one eventuallyEq_nhdsWithin_iff Metric.eventually_nhds_iff zero_lt_one norm_eq_abs lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt abs_sub_lt_iff dist_eq Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.sub_nonpos_of_le HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_arctan tsum_mul_right mul_assoc div_mul_eq_mul_div arctan_one tendsto_nhds_unique nhdsLT_neBot LinearOrderedSemiField.toDenselyOrdered instNoMinOrderOfNontrivial Filter.Tendsto.mono_left Continuous.tendsto continuous_arctan

---

← Back to Index