Basic

📁 Source: Mathlib/Analysis/SpecificLimits/Basic.lean

Statistics

Metric	Count
Definitions `posSumOfEncodable`	1
Theorems `eq_zero_of_le_mul_pow`, `exists_pos_sum_of_countable`, `exists_pos_sum_of_countable'`, `exists_pos_tsum_mul_lt_of_countable`, `tendsto_pow_atTop_nhds_top_iff`, `tendsto_pow_atTop_nhds_zero_iff`, `tendsto_pow_atTop_nhds_zero_of_lt_one`, `tsum_geometric`, `tsum_geometric_add_one`, `tsum_geometric_two`, `tsum_geometric_two_encode_le_two`, `tsum_two_zpow_neg_add_one`, `tendsto_const_div_atTop_nhds_zero_nat`, `div_mul_cancel`, `div_mul_cancel_atTop`, `den`, `num`, `num_atTop_iff_den_atTop`, `tendsto_algebraMap_inv_atTop_nhds_zero_nat`, `tendsto_inv_atTop_nhds_zero_nat`, `exists_pos_sum_of_countable`, `hasSum_geometric`, `summable_geometric`, `tendsto_algebraMap_inverse_atTop_nhds_zero_nat`, `tendsto_const_div_atTop_nhds_zero_nat`, `tendsto_inverse_atTop_nhds_zero_nat`, `tendsto_pow_atTop_nhds_zero_iff`, `tendsto_pow_atTop_nhds_zero_of_lt_one`, `tendsto_div_const_atTop`, `tendsto_pow_atTop_atTop_of_one_lt`, `exists_pos_forall_sum_le`, `exists_pos_hasSum_le`, `aux_hasSum_of_le_geometric`, `cauchySeq_of_edist_le_geometric`, `cauchySeq_of_edist_le_geometric_two`, `cauchySeq_of_le_geometric`, `cauchySeq_of_le_geometric_two`, `dist_le_of_le_geometric_of_tendsto`, `dist_le_of_le_geometric_of_tendsto₀`, `dist_le_of_le_geometric_two_of_tendsto`, `dist_le_of_le_geometric_two_of_tendsto₀`, `edist_le_of_edist_le_geometric_of_tendsto`, `edist_le_of_edist_le_geometric_of_tendsto₀`, `edist_le_of_edist_le_geometric_two_of_tendsto`, `edist_le_of_edist_le_geometric_two_of_tendsto₀`, `factorial_tendsto_atTop`, `geom_le`, `geom_lt`, `hasSum_geometric_of_lt_one`, `hasSum_geometric_two`, `hasSum_geometric_two'`, `le_geom`, `lt_geom`, `sum_geometric_two_le`, `summable_geometric_of_lt_one`, `summable_geometric_two`, `summable_geometric_two'`, `summable_geometric_two_encode`, `summable_one_div_pow_of_le`, `tendsto_add_mul_div_add_mul_atTop_nhds`, `tendsto_add_one_pow_atTop_atTop_of_pos`, `tendsto_algebraMap_inv_atTop_nhds_zero_nat`, `tendsto_algebraMap_inverse_atTop_nhds_zero_nat`, `tendsto_atTop_of_geom_le`, `tendsto_const_div_atTop_nhds_zero_nat`, `tendsto_factorial_div_pow_self_atTop`, `tendsto_inv_atTop_nhds_zero_nat`, `tendsto_inverse_atTop_nhds_zero_nat`, `tendsto_mod_div_atTop_nhds_zero_nat`, `tendsto_mul_add_inv_atTop_nhds_zero`, `tendsto_natCast_div_add_atTop`, `tendsto_nat_ceil_atTop`, `tendsto_nat_ceil_div_atTop`, `tendsto_nat_ceil_mul_div_atTop`, `tendsto_nat_floor_atTop`, `tendsto_nat_floor_div_atTop`, `tendsto_nat_floor_mul_atTop`, `tendsto_nat_floor_mul_div_atTop`, `tendsto_one_div_add_atTop_nhds_zero_nat`, `tendsto_one_div_atTop_nhds_zero_nat`, `tendsto_pow_atTop_atTop_of_one_lt`, `tendsto_pow_atTop_nhdsWithin_zero_of_lt_one`, `tendsto_pow_atTop_nhds_zero_iff`, `tendsto_pow_atTop_nhds_zero_of_lt_one`, `tsum_geometric_encode_lt_top`, `tsum_geometric_inv_two`, `tsum_geometric_inv_two_ge`, `tsum_geometric_lt_top`, `tsum_geometric_nnreal`, `tsum_geometric_of_lt_one`, `tsum_geometric_two`, `tsum_geometric_two'`, `uniformity_basis_dist_pow_of_lt_one`	93
Total	94

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_le_mul_pow` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Preorder.toLE` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `ofNNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`instZeroENNReal`	—	`nonpos_iff_eq_zero` `instCanonicallyOrderedAdd` `ge_of_tendsto'` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopology` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `MulZeroClass.mul_zero` `Tendsto.const_mul` `tendsto_pow_atTop_nhds_zero_of_lt_one` `coe_ne_top`
`exists_pos_sum_of_countable` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `ENNReal` `instPartialOrder` `tsum` `instAddCommMonoid` `instTopologicalSpace` `ofNNReal` `SummationFilter.unconditional`	—	`exists_between` `instDenselyOrdered` `pos_iff_ne_zero` `instCanonicallyOrderedAdd` `lt_iff_exists_coe` `NNReal.exists_pos_sum_of_countable` `LT.lt.ne'` `coe_pos` `lt_trans` `coe_lt_coe` `tsum_coe_eq`
`exists_pos_sum_of_countable'` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `instZeroENNReal` `tsum` `instAddCommMonoid` `instTopologicalSpace` `SummationFilter.unconditional`	—	`exists_pos_sum_of_countable` `coe_pos`
`exists_pos_tsum_mul_lt_of_countable` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `ENNReal` `instPartialOrder` `tsum` `instAddCommMonoid` `instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `ofNNReal` `SummationFilter.unconditional`	—	`CanLift.prf` `Pi.canLift` `canLift` `exists_pos_sum_of_countable` `LT.lt.trans_le` `zero_lt_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `le_max_left` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `lt_of_le_of_lt` `tsum_le_tsum` `coe_div` `LT.lt.ne'` `mul_le_of_le_div'` `le_imp_le_of_le_of_le` `div_le_div` `le_refl` `coe_le_coe_of_le` `le_max_right`
`tendsto_pow_atTop_nhds_top_iff` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `instTopologicalSpace` `Top.top` `instTopENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Ioi_mem_nhds` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopology` `one_lt_top` `lt_irrefl` `lt_of_lt_of_le` `le_rfl` `pow_le_one₀` `IsOrderedRing.toPosMulMono` `instIsOrderedRing` `zero_le` `instCanonicallyOrderedAdd` `Filter.Tendsto.inv` `instContinuousInv` `inv_inv` `inv_zero` `inv_lt_one`
`tendsto_pow_atTop_nhds_zero_iff` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `instTopologicalSpace` `instZeroENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`CanLift.prf` `canLift` `top_ne_zero` `tendsto_nhds_unique` `instT2Space` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.EventuallyEq.tendsto` `Filter.eventually_atTop` `pow_eq_top_iff` `Nat.cast_one` `NNReal.tendsto_pow_atTop_nhds_zero_iff` `Nat.cast_zero` `coe_zero` `tendsto_pow_atTop_nhds_zero_of_lt_one`
`tendsto_pow_atTop_nhds_zero_of_lt_one` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `instTopologicalSpace` `instZeroENNReal`	—	`lt_iff_exists_coe` `coe_zero` `Nat.cast_zero` `NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one` `Nat.cast_one`
`tsum_geometric` 📖	mathematical	—	`tsum` `ENNReal` `instAddCommMonoid` `instTopologicalSpace` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiring` `SummationFilter.unconditional` `instInv` `instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`lt_or_ge` `lt_iff_exists_coe` `Nat.cast_one` `coe_inv` `ne_of_gt` `tsub_pos_iff_lt` `NNReal.instCanonicallyOrderedAdd` `NNReal.instOrderedSub` `coe_sub` `coe_one` `tsum_coe_eq` `NNReal.hasSum_geometric` `tsub_eq_zero_iff_le` `instCanonicallyOrderedAdd` `instOrderedSub` `inv_zero` `tsum_eq_iSup_nat` `iSup_eq_top` `lt_of_lt_of_le` `Finset.sum_const` `nsmul_one` `Finset.card_range` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `one_le_pow₀` `IsOrderedRing.toZeroLEOneClass` `instIsOrderedRing` `IsOrderedRing.toPosMulMono` `exists_nat_gt` `lt_top_iff_ne_top`
`tsum_geometric_add_one` 📖	mathematical	—	`tsum` `ENNReal` `instAddCommMonoid` `instTopologicalSpace` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiring` `SummationFilter.unconditional` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instInv` `instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`pow_succ'` `tsum_mul_left` `tsum_geometric`
`tsum_geometric_two` 📖	mathematical	—	`tsum` `ENNReal` `instAddCommMonoid` `instTopologicalSpace` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiring` `instInv` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `tsum_geometric` `one_sub_inv_two` `inv_inv`
`tsum_geometric_two_encode_le_two` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `tsum` `instAddCommMonoid` `instTopologicalSpace` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiring` `instInv` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `Encodable.encode` `SummationFilter.unconditional`	—	`LE.le.trans_eq` `Nat.instAtLeastTwoHAddOfNat` `tsum_comp_le_tsum_of_injective` `Encodable.encode_injective` `tsum_geometric_two`
`tsum_two_zpow_neg_add_one` 📖	mathematical	—	`tsum` `ENNReal` `instAddCommMonoid` `instTopologicalSpace` `DivInvMonoid.toZPow` `instDivInvMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `SummationFilter.unconditional` `AddMonoidWithOne.toOne`	—	`Nat.instAtLeastTwoHAddOfNat` `neg_sub_left` `zpow_neg` `Nat.cast_one` `zpow_natCast` `inv_pow` `tsum_geometric_add_one` `one_sub_inv_two` `inv_inv` `inv_mul_cancel` `CharZero.NeZero.two` `instCharZero` `top_ne_ofNat`

EReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_const_div_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `EReal` `DivInvMonoid.toDiv` `instDivInvMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneEReal` `Filter.atTop` `Nat.instPreorder` `nhds` `instTopologicalSpace` `instZeroEReal`	—	`coe_toReal` `coe_coe_eq_natCast` `coe_div` `coe_zero` `tendsto_coe` `tendsto_const_div_atTop_nhds_zero_nat` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `NNRat.instContinuousSMulOfIsScalarTowerOfRat` `IsScalarTower.nnrat` `Rat.instCharZero` `NNRat.instContinuousSMulRatReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`div_mul_cancel` 📖	mathematical	`Filter.Tendsto` `Filter.principal` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`Filter.EventuallyEq` `MulZeroClass.toMul` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`Filter.mp_mem` `Filter.Tendsto.le_comap` `Filter.preimage_mem_comap` `Filter.mem_principal_self` `Filter.univ_mem'` `IsUnit.div_mul_cancel`
`div_mul_cancel_atTop` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filter.EventuallyEq` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero`	—	`div_mul_cancel` `Filter.Tendsto.mono_right` `Filter.le_principal_iff` `Filter.mem_of_superset` `Filter.Ioi_mem_atTop` `instNoTopOrderOfNoMaxOrder` `IsStrictOrderedRing.toNoMaxOrder`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`den` 📖	—	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `nhds`	—	—	`inv_div` `inv` `congr'` `Filter.EventuallyEq.div_mul_cancel_atTop` `pos_mul_atTop` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono`
`num` 📖	—	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `nhds`	—	—	`congr'` `Filter.EventuallyEq.div_mul_cancel_atTop` `pos_mul_atTop`
`num_atTop_iff_den_atTop` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `nhds`	`Filter.atTop`	—	`den` `num`

NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_algebraMap_inv_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `NNRat` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringNNRat` `RingHom.instFunLike` `algebraMap` `instInv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemifield` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Filter.Tendsto.comp` `ContinuousAt.tendsto` `Continuous.continuousAt` `continuous_algebraMap` `tendsto_inv_atTop_nhds_zero_nat`
`tendsto_inv_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `NNRat` `instInv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instSemifield` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`Filter.Tendsto.comp` `tendsto_inv_atTop_zero` `instIsStrictOrderedRingNNRat` `instOrderTopology` `tendsto_natCast_atTop_atTop` `IsStrictOrderedRing.toIsOrderedRing` `instArchimedeanNNRat`

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_pos_sum_of_countable` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instTopologicalSpace` `SummationFilter.unconditional`	—	`nonempty_encodable` `exists_between` `instDenselyOrdered` `pos_iff_ne_zero` `instCanonicallyOrderedAdd` `LT.lt.le` `coe_lt_coe` `hasSum_le` `Real.instIsOrderedAddMonoid` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `hasSum_zero` `SummationFilter.instNeBotUnconditional` `hasSum_coe` `LT.lt.trans_le'` `coe_le_coe`
`hasSum_geometric` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`HasSum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instTopologicalSpace` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instInv` `instSub` `SummationFilter.unconditional`	—	`hasSum_coe` `coe_sub` `le_of_lt` `hasSum_geometric_of_lt_one` `coe_nonneg`
`summable_geometric` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`Summable` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `instTopologicalSpace` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SummationFilter.unconditional`	—	`hasSum_geometric`
`tendsto_algebraMap_inverse_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `algebraMap` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`tendsto_algebraMap_inv_atTop_nhds_zero_nat`
`tendsto_const_div_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`tendsto_const_div_atTop_nhds_zero_nat`
`tendsto_inverse_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`tendsto_inv_atTop_nhds_zero_nat`
`tendsto_pow_atTop_nhds_zero_iff` 📖	mathematical	—	`Filter.Tendsto` `NNReal` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `Filter.atTop` `Nat.instPreorder` `nhds` `instTopologicalSpace` `instZeroNNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	—	`abs_eq` `tendsto_pow_atTop_nhds_zero_iff` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `instOrderTopologyReal` `tendsto_coe` `tendsto_pow_atTop_nhds_zero_of_lt_one`
`tendsto_pow_atTop_nhds_zero_of_lt_one` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `Filter.atTop` `Nat.instPreorder` `nhds` `instTopologicalSpace` `instZeroNNReal`	—	`tendsto_coe` `tendsto_pow_atTop_nhds_zero_of_lt_one` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Real.instArchimedean` `instOrderTopologyReal` `coe_nonneg`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_div_const_atTop` 📖	mathematical	—	`Filter.Tendsto` `Filter.atTop` `instPreorder`	—	`Filter.Tendsto.eq_1` `Filter.map_div_atTop_eq_nat` `Ne.bot_lt` `le_refl`
`tendsto_pow_atTop_atTop_of_one_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Filter.atTop` `instPreorder`	—	`tendsto_pow_atTop_atTop_of_one_lt`

Set.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_pos_forall_sum_le` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instLE` `Finset.sum` `Real.instAddCommMonoid`	—	`exists_pos_hasSum_le` `Finset.sum_subtype_of_mem` `LE.le.trans` `sum_le_hasSum` `Real.instIsOrderedAddMonoid` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `SummationFilter.instNeBotUnconditional` `SummationFilter.instLeAtTopUnconditional` `LT.lt.le`
`exists_pos_hasSum_le` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`HasSum` `Set.Elem` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set` `Set.instMembership` `SummationFilter.unconditional` `Real.instLE`	—	`zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Subtype.coe_eta`

(root)

Definitions

Name	Category	Theorems
`posSumOfEncodable` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aux_hasSum_of_le_geometric` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	`HasSum` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub` `SummationFilter.unconditional`	—	`sign_cases_of_C_mul_pow_nonneg` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LE.le.trans` `dist_nonneg` `MulZeroClass.zero_mul` `zero_div` `HasSum.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `hasSum_geometric_of_lt_one`
`cauchySeq_of_edist_le_geometric` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Preorder.toLE` `EDist.edist` `PseudoEMetricSpace.toEDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`CauchySeq` `PseudoEMetricSpace.toUniformSpace` `Nat.instPreorder`	—	`cauchySeq_of_edist_le_of_tsum_ne_top` `ENNReal.tsum_mul_left` `ENNReal.tsum_geometric` `LT.lt.ne'` `tsub_pos_iff_lt` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instOrderedSub` `ENNReal.mul_ne_top` `ENNReal.Finiteness.inv_ne_top`
`cauchySeq_of_edist_le_geometric_two` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`CauchySeq` `PseudoEMetricSpace.toUniformSpace` `Nat.instPreorder`	—	`Nat.instAtLeastTwoHAddOfNat` `cauchySeq_of_edist_le_geometric` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `ENNReal.instCharZero` `div_eq_mul_inv` `ENNReal.inv_pow`
`cauchySeq_of_le_geometric` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	`CauchySeq` `PseudoMetricSpace.toUniformSpace` `Nat.instPreorder`	—	`cauchySeq_of_dist_le_of_summable` `aux_hasSum_of_le_geometric`
`cauchySeq_of_le_geometric_two` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `Real.instMonoid`	`CauchySeq` `PseudoMetricSpace.toUniformSpace` `Nat.instPreorder`	—	`Nat.instAtLeastTwoHAddOfNat` `cauchySeq_of_dist_le_of_summable` `hasSum_geometric_two'`
`dist_le_of_le_geometric_of_tendsto` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub`	—	`aux_hasSum_of_le_geometric` `mul_div_right_comm` `pow_add` `mul_left_comm` `mul_comm` `HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `HasSum.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `dist_le_tsum_of_dist_le_of_tendsto`
`dist_le_of_le_geometric_of_tendsto₀` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub`	—	`dist_le_tsum_of_dist_le_of_tendsto₀` `aux_hasSum_of_le_geometric` `HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional`
`dist_le_of_le_geometric_two_of_tendsto` 📖	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `Real.instMonoid` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	—	`Nat.instAtLeastTwoHAddOfNat` `add_comm` `pow_add` `HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `HasSum.div_const` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `hasSum_geometric_two'` `dist_le_tsum_of_dist_le_of_tendsto` `summable_geometric_two'`
`dist_le_of_le_geometric_two_of_tendsto₀` 📖	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `Real.instMonoid` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	—	`Nat.instAtLeastTwoHAddOfNat` `dist_le_tsum_of_dist_le_of_tendsto₀` `summable_geometric_two'` `tsum_geometric_two'`
`edist_le_of_edist_le_geometric_of_tendsto` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `ENNReal.instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`div_eq_mul_inv` `mul_assoc` `pow_add` `ENNReal.tsum_mul_left` `ENNReal.tsum_geometric` `edist_le_tsum_of_edist_le_of_tendsto`
`edist_le_of_edist_le_geometric_of_tendsto₀` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `ENNReal.instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`pow_zero` `mul_one` `edist_le_of_edist_le_geometric_of_tendsto`
`edist_le_of_edist_le_geometric_two_of_tendsto` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Nat.instAtLeastTwoHAddOfNat` `div_eq_mul_inv` `ENNReal.inv_pow` `mul_assoc` `mul_comm` `ENNReal.one_sub_inv_two` `inv_inv` `edist_le_of_edist_le_geometric_of_tendsto`
`edist_le_of_edist_le_geometric_two_of_tendsto₀` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Nat.instAtLeastTwoHAddOfNat` `pow_zero` `div_eq_mul_inv` `inv_one` `mul_one` `edist_le_of_edist_le_geometric_two_of_tendsto`
`factorial_tendsto_atTop` 📖	mathematical	—	`Filter.Tendsto` `Nat.factorial` `Filter.atTop` `Nat.instPreorder`	—	`Filter.tendsto_atTop_atTop_of_monotone` `Nat.factorial_le` `Nat.self_le_factorial`
`geom_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instMul`	`Monoid.toNatPow` `Real.instMonoid`	—	`Monotone.seq_le_seq` `monotone_mul_left_of_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `pow_zero` `one_mul` `pow_succ'` `mul_assoc`
`geom_lt` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Real.instMul`	`Monoid.toNatPow` `Real.instMonoid`	—	`Monotone.seq_pos_lt_seq_of_le_of_lt` `monotone_mul_left_of_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `pow_zero` `one_mul` `pow_succ'` `mul_assoc`
`hasSum_geometric_of_lt_one` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Real.instOne`	`HasSum` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `Real.instInv` `Real.instSub` `SummationFilter.unconditional`	—	`ne_of_lt` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `tendsto_pow_atTop_nhds_zero_of_lt_one` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Real.instArchimedean` `instOrderTopologyReal` `tendsto_const_nhds` `hasSum_iff_tendsto_nat_of_nonneg` `pow_nonneg` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `geom_sum_eq` `div_eq_mul_inv` `zero_sub` `neg_mul` `one_mul` `neg_inv` `neg_sub`
`hasSum_geometric_two` 📖	mathematical	—	`HasSum` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `hasSum_geometric_of_lt_one` `Mathlib.Meta.NormNum.isRat_le_true` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero`
`hasSum_geometric_two'` 📖	mathematical	—	`HasSum` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `Real.instMonoid` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `one_div` `inv_pow` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `IsUnit.div_mul_cancel` `Mathlib.Meta.NormNum.isNat_eq_false` `Nat.cast_zero` `HasSum.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `hasSum_geometric_of_lt_one` `le_of_lt` `one_half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `one_half_lt_one`
`le_geom` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instMul`	`Monoid.toNatPow` `Real.instMonoid`	—	`Monotone.seq_le_seq` `monotone_mul_left_of_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `pow_zero` `one_mul` `pow_succ'` `mul_assoc`
`lt_geom` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Real.instMul`	`Monoid.toNatPow` `Real.instMonoid`	—	`Monotone.seq_pos_lt_seq_of_lt_of_le` `monotone_mul_left_of_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `pow_zero` `one_mul` `pow_succ'` `mul_assoc`
`sum_geometric_two_le` 📖	mathematical	—	`Real` `Real.instLE` `Finset.sum` `Real.instAddCommMonoid` `Finset.range` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `pow_nonneg` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isRat_le_true` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.instAtLeastTwo` `tsum_geometric_two` `Summable.sum_le_tsum` `Real.instIsOrderedAddMonoid` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `SummationFilter.instNeBotUnconditional` `SummationFilter.instLeAtTopUnconditional` `summable_geometric_two`
`summable_geometric_of_lt_one` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Real.instOne`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `SummationFilter.unconditional`	—	`hasSum_geometric_of_lt_one`
`summable_geometric_two` 📖	mathematical	—	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `hasSum_geometric_two`
`summable_geometric_two'` 📖	mathematical	—	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `Real.instMonoid` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `hasSum_geometric_two'`
`summable_geometric_two_encode` 📖	mathematical	—	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Encodable.encode` `SummationFilter.unconditional`	—	`Summable.comp_injective` `instIsUniformAddGroupReal` `Nat.instAtLeastTwoHAddOfNat` `Real.instCompleteSpace` `summable_geometric_two` `Encodable.encode_injective`
`summable_one_div_pow_of_le` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`Summable` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `SummationFilter.unconditional`	—	`Summable.of_nonneg_of_le` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `lt_trans` `div_pow` `one_pow` `one_div_le_one_div` `Real.instZeroLEOneClass` `LT.lt.trans` `zero_lt_one` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `pow_right_mono₀` `IsOrderedRing.toPosMulMono` `LT.lt.le` `summable_geometric_of_lt_one` `one_div_nonneg` `LE.le.trans` `zero_le_one` `one_div_lt` `LE.le.trans_lt` `Eq.le` `one_div_one`
`tendsto_add_mul_div_add_mul_atTop_nhds` 📖	mathematical	—	`Filter.Tendsto` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Distrib.toMul` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`Filter.Tendsto.congr'` `Filter.Eventually.mp` `Filter.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Filter.Eventually.of_forall` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Nat.cast_zero` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.atom_pf'` `Filter.Tendsto.div` `IsTopologicalSemiring.toContinuousMul` `Filter.Tendsto.add_const` `IsTopologicalSemiring.toContinuousAdd` `Filter.Tendsto.const_mul` `tendsto_inv_atTop_nhds_zero_nat` `MulZeroClass.mul_zero` `zero_add`
`tendsto_add_one_pow_atTop_atTop_of_pos` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Filter.atTop` `Nat.instPreorder`	—	`Filter.tendsto_atTop_atTop_of_monotone'` `pow_right_mono₀` `IsStrictOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `le_add_of_nonneg_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `LT.lt.le` `not_bddAbove_iff` `Set.exists_range_iff` `add_one_pow_unbounded_of_pos`
`tendsto_algebraMap_inv_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `algebraMap` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Filter.Tendsto.comp` `ContinuousAt.tendsto` `Continuous.continuousAt` `continuous_algebraMap` `tendsto_inv_atTop_nhds_zero_nat`
`tendsto_algebraMap_inverse_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `algebraMap` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`tendsto_algebraMap_inv_atTop_nhds_zero_nat`
`tendsto_atTop_of_geom_le` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instOne` `Real.instLE` `Real.instMul`	`Filter.Tendsto` `Filter.atTop` `Nat.instPreorder` `Real.instPreorder`	—	`Filter.tendsto_atTop_mono` `geom_le` `LE.le.trans` `zero_le_one` `Real.instZeroLEOneClass` `LT.lt.le` `Filter.Tendsto.atTop_mul_const` `Real.instIsStrictOrderedRing` `tendsto_pow_atTop_atTop_of_one_lt` `AddGroup.existsAddOfLE` `Real.instArchimedean`
`tendsto_const_div_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`div_eq_mul_inv` `MulZeroClass.mul_zero` `Filter.Tendsto.mul` `tendsto_const_nhds` `tendsto_inv_atTop_nhds_zero_nat`
`tendsto_factorial_div_pow_self_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `Nat.factorial` `Monoid.toNatPow` `Real.instMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`tendsto_of_tendsto_of_tendsto_of_le_of_le'` `instOrderTopologyReal` `tendsto_const_nhds` `tendsto_const_div_atTop_nhds_zero_nat` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `NNRat.instContinuousSMulOfIsScalarTowerOfRat` `IsScalarTower.nnrat` `Rat.instCharZero` `NNRat.instContinuousSMulRatReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Filter.Eventually.of_forall` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `LT.lt.le` `Nat.factorial_pos` `pow_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Filter.Eventually.mono` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `LT.lt.ne` `Nat.factorial_eq_prod_range_add_one` `Finset.pow_eq_prod_const` `div_eq_mul_inv` `inv_eq_one_div` `Finset.prod_natCast` `Nat.cast_succ` `Finset.prod_inv_distrib` `Finset.prod_mul_distrib` `Finset.prod_range_succ'` `Finset.prod_congr` `Nat.cast_add` `Nat.cast_one` `zero_add` `one_mul` `mul_le_of_le_one_left` `IsOrderedRing.toMulPosMono` `inv_nonneg` `Finset.prod_le_one` `le_of_lt` `mul_pos` `add_pos'` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Nat.cast_nonneg'` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `inv_pos_of_pos` `div_le_one` `Finset.mem_range`
`tendsto_inv_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_natCast` `NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat`
`tendsto_inverse_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`tendsto_inv_atTop_nhds_zero_nat`
`tendsto_mod_div_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`Real.instIsOrderedRing` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_bdd_div_atTop_nhds_zero` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `Filter.Eventually.of_forall` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `LT.lt.le` `tendsto_natCast_atTop_atTop` `Real.instArchimedean`
`tendsto_mul_add_inv_atTop_nhds_zero` 📖	mathematical	—	`Filter.Tendsto` `Real` `Real.instInv` `Real.instAdd` `Real.instMul` `Filter.atTop` `Real.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`lt_or_gt_of_ne` `Filter.Tendsto.comp` `tendsto_inv_atBot_zero` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `Filter.tendsto_atBot_add_const_right` `Real.instIsOrderedAddMonoid` `Filter.Tendsto.const_mul_atTop_of_neg` `Filter.tendsto_id` `tendsto_inv_atTop_zero` `Filter.tendsto_atTop_add_const_right` `Filter.Tendsto.const_mul_atTop`
`tendsto_natCast_div_add_atTop` 📖	mathematical	—	`Filter.Tendsto` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Filter.atTop` `Nat.instPreorder` `nhds` `AddMonoidWithOne.toOne`	—	`Filter.Tendsto.congr'` `Filter.Eventually.mp` `Filter.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Filter.Eventually.of_forall` `add_div'` `Nat.cast_ne_zero` `one_mul` `one_div` `inv_div` `MulZeroClass.mul_zero` `add_zero` `div_one` `Filter.Tendsto.div` `IsTopologicalSemiring.toContinuousMul` `tendsto_const_nhds` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `div_eq_mul_inv` `Filter.Tendsto.mul` `Filter.Tendsto.comp` `Continuous.tendsto` `continuous_algebraMap` `tendsto_inv_atTop_nhds_zero_nat` `NNRat.instCharZero` `ContinuousMul.to_continuousSMul` `NNRat.instIsTopologicalSemiring` `Filter.tendsto_atTop'` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_natCast` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `NeZero.charZero_one`
`tendsto_nat_ceil_atTop` 📖	mathematical	—	`Filter.Tendsto` `Nat.ceil` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.atTop` `PartialOrder.toPreorder` `Nat.instPreorder`	—	`Monotone.tendsto_atTop_atTop` `Nat.ceil_mono` `Nat.ceil_natCast`
`tendsto_nat_ceil_div_atTop` 📖	mathematical	—	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Nat.ceil` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `FloorRing.toFloorSemiring` `Filter.atTop` `PartialOrder.toPreorder` `nhds` `AddMonoidWithOne.toOne`	—	`one_mul` `tendsto_nat_ceil_mul_div_atTop` `zero_le_one'` `IsStrictOrderedRing.toZeroLEOneClass`
`tendsto_nat_ceil_mul_div_atTop` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Nat.ceil` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `FloorRing.toFloorSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Filter.atTop` `nhds`	—	`Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `IsStrictOrderedRing.toIsTopologicalDivisionRing` `tendsto_const_nhds` `tendsto_inv_atTop_zero` `tendsto_of_tendsto_of_tendsto_of_le_of_le'` `add_zero` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `FloorRing.archimedean` `Nontrivial.to_nonempty` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `LT.lt.trans_le` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Nat.le_ceil` `div_le_iff₀` `add_mul` `Distrib.rightDistribClass` `inv_mul_cancel₀` `LT.lt.ne'` `LT.lt.le` `Nat.ceil_lt_add_one` `mul_nonneg` `IsOrderedRing.toPosMulMono` `LE.le.trans` `zero_le_one`
`tendsto_nat_floor_atTop` 📖	mathematical	—	`Filter.Tendsto` `Nat.floor` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.atTop` `PartialOrder.toPreorder` `Nat.instPreorder`	—	`Monotone.tendsto_atTop_atTop` `Nat.floor_mono` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `IsCancelAdd.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toIsCancelAdd` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le`
`tendsto_nat_floor_div_atTop` 📖	mathematical	—	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Nat.floor` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `FloorRing.toFloorSemiring` `Filter.atTop` `PartialOrder.toPreorder` `nhds` `AddMonoidWithOne.toOne`	—	`one_mul` `tendsto_nat_floor_mul_div_atTop` `zero_le_one'` `IsStrictOrderedRing.toZeroLEOneClass`
`tendsto_nat_floor_mul_atTop` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	`Filter.Tendsto` `Nat.floor` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Filter.atTop` `Nat.instPreorder`	—	`Filter.Tendsto.comp` `tendsto_nat_floor_atTop` `Filter.Tendsto.const_mul_atTop` `tendsto_natCast_atTop_atTop` `IsStrictOrderedRing.toIsOrderedRing`
`tendsto_nat_floor_mul_div_atTop` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Filter.Tendsto` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Nat.floor` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `FloorRing.toFloorSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Filter.atTop` `nhds`	—	`Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `LinearOrderedAddCommGroup.toIsTopologicalAddGroup` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `tendsto_const_nhds` `tendsto_inv_atTop_zero` `tendsto_of_tendsto_of_tendsto_of_le_of_le'` `sub_zero` `Filter.eventually_atTop` `instIsDirectedOrder` `FloorRing.archimedean` `Nontrivial.to_nonempty` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `LT.lt.trans_le` `zero_lt_one` `IsStrictOrderedRing.toZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `sub_mul` `inv_mul_cancel₀` `LT.lt.ne'` `Nat.lt_floor_add_one` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `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_mul` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `div_le_iff₀` `Nat.floor_le` `mul_nonneg` `IsOrderedRing.toPosMulMono` `LE.le.trans` `zero_le_one`
`tendsto_one_div_add_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Filter.tendsto_add_atTop_iff_nat` `tendsto_one_div_atTop_nhds_zero_nat` `one_div` `Nat.cast_add` `Nat.cast_one`
`tendsto_one_div_atTop_nhds_zero_nat` 📖	mathematical	—	`Filter.Tendsto` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `AddMonoidWithOne.toNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`one_div`
`tendsto_pow_atTop_atTop_of_one_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Filter.atTop` `Nat.instPreorder`	—	`exists_pos_add_of_lt'` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `add_comm` `tendsto_add_one_pow_atTop_atTop_of_pos`
`tendsto_pow_atTop_nhdsWithin_zero_of_lt_one` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Filter.atTop` `Nat.instPreorder` `nhdsWithin` `Set.Ioi`	—	`Filter.tendsto_inf` `tendsto_pow_atTop_nhds_zero_of_lt_one` `LT.lt.le` `Filter.tendsto_principal` `Filter.Eventually.of_forall` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass`
`tendsto_pow_atTop_nhds_zero_iff` 📖	mathematical	—	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Filter.atTop` `Nat.instPreorder` `nhds` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`tendsto_zero_iff_abs_tendsto_zero` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `by_contra` `zero_ne_one` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `tendsto_nhds_unique` `T25Space.t2Space` `T3Space.t25Space` `T4Space.t3Space` `T5Space.toT4Space` `OrderTopology.t5Space` `Filter.atTop_neBot` `instIsDirectedOrder` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `one_pow` `tendsto_const_nhds` `not_tendsto_nhds_of_tendsto_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `Monotone.tendsto_atTop_atTop` `StrictMono.monotone` `pow_right_strictMono₀` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `lt_of_le_of_ne` `le_of_not_gt` `pow_unbounded_of_one_lt` `AddGroup.existsAddOfLE` `le_of_lt` `tendsto_pow_atTop_nhds_zero_of_lt_one` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`tendsto_pow_atTop_nhds_zero_of_lt_one` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Preorder.toLT` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Filter.Tendsto` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`LE.le.eq_or_lt` `Filter.tendsto_add_atTop_iff_nat` `pow_succ` `MulZeroClass.mul_zero` `T5Space.toT1Space` `OrderTopology.t5Space` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_pow_atTop_atTop_of_one_lt` `one_lt_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Filter.Tendsto.congr` `inv_pow` `inv_inv` `Filter.Tendsto.comp` `tendsto_inv_atTop_zero`
`tsum_geometric_encode_lt_top` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Encodable.encode` `SummationFilter.unconditional` `Top.top` `instTopENNReal`	—	`LE.le.trans_lt` `ENNReal.tsum_comp_le_tsum_of_injective` `Encodable.encode_injective` `ENNReal.tsum_geometric` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instOrderedSub`
`tsum_geometric_inv_two` 📖	mathematical	—	`tsum` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `tsum_geometric_two` `inv_eq_one_div`
`tsum_geometric_inv_two_ge` 📖	mathematical	—	`tsum` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instZero` `SummationFilter.unconditional` `Real.instMul`	—	`Nat.instAtLeastTwoHAddOfNat` `one_div` `Summable.indicator` `instIsUniformAddGroupReal` `Real.instCompleteSpace` `summable_geometric_two` `Finset.sum_eq_zero` `lt_irrefl` `LT.lt.trans_le` `Finset.mem_range` `Summable.sum_add_tsum_nat_add` `instIsTopologicalAddGroupReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `pow_add` `tsum_mul_right` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tsum_geometric_inv_two` `zero_add`
`tsum_geometric_lt_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `SummationFilter.unconditional` `Top.top` `instTopENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`ENNReal.tsum_geometric` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instOrderedSub`
`tsum_geometric_nnreal` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`tsum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instTopologicalSpace` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SummationFilter.unconditional` `NNReal.instInv` `NNReal.instSub`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `NNReal.hasSum_geometric`
`tsum_geometric_of_lt_one` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instLT` `Real.instOne`	`tsum` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `SummationFilter.unconditional` `Real.instInv` `Real.instSub`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_geometric_of_lt_one`
`tsum_geometric_two` 📖	mathematical	—	`tsum` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `Nat.instAtLeastTwoHAddOfNat` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_geometric_two`
`tsum_geometric_two'` 📖	mathematical	—	`tsum` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `Real.instMonoid` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `Nat.instAtLeastTwoHAddOfNat` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_geometric_two'`
`uniformity_basis_dist_pow_of_lt_one` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instOne`	`Filter.HasBasis` `uniformity` `PseudoMetricSpace.toUniformSpace` `setOf` `Dist.dist` `PseudoMetricSpace.toDist` `Monoid.toNatPow` `Real.instMonoid`	—	`Metric.mk_uniformity_basis` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instZeroLEOneClass` `LT.lt.le` `exists_pow_lt_of_lt_one` `Real.instArchimedean` `AddGroup.existsAddOfLE`

---

← Back to Index