RCLike

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

Statistics

Metric	Count
Definitions	0
Theorems tendsto_add_mul_div_add_mul_atTop_nhds, tendsto_inverse_atTop_nhds_zero_nat, tendsto_ofReal_atBot_cobounded, tendsto_ofReal_atTop_cobounded, tendsto_ofReal_cobounded_cobounded	5
Total	5

RCLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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	—	tendsto_add_mul_div_add_mul_atTop_nhds
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_ofReal_atBot_cobounded 📖	mathematical	—	Filter.Tendsto Real ofReal Filter.atBot Real.instPreorder Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField	—	tendsto_norm_atTop_iff_cobounded norm_ofReal Filter.tendsto_abs_atBot_atTop Real.instIsOrderedAddMonoid
tendsto_ofReal_atTop_cobounded 📖	mathematical	—	Filter.Tendsto Real ofReal Filter.atTop Real.instPreorder Bornology.cobounded PseudoMetricSpace.toBornology SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField	—	tendsto_norm_atTop_iff_cobounded norm_ofReal Filter.tendsto_abs_atTop_atTop
tendsto_ofReal_cobounded_cobounded 📖	mathematical	—	Filter.Tendsto Real ofReal Bornology.cobounded PseudoMetricSpace.toBornology Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField toDenselyNormedField	—	tendsto_norm_atTop_iff_cobounded norm_ofReal tendsto_norm_cobounded_atTop

---

← Back to Index