Lemmas

📁 Source: Mathlib/Tactic/ComputeAsymptotics/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems isBigOWith_of_tendsto_bot, isBigOWith_of_tendsto_top, isBigO_of_div_tendsto_atBot, isBigO_of_div_tendsto_atTop, tendsto_nhdsGT_of_tendsto_atTop, tendsto_nhdsLT_of_tendsto_atTop, tendsto_nhdsNE_of_tendsto_atTop, tendsto_nhdsNE_of_tendsto_atTop_nhds_of_eq	8
Total	8

Tactic.ComputeAsymptotics

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBigOWith_of_tendsto_bot 📖	mathematical	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Filter.atBot Real.instPreorder Real.instLT Real.instZero	Asymptotics.IsBigOWith Real Real.norm	—	Asymptotics.IsLittleO.forall_isBigOWith Asymptotics.IsLittleO.of_tendsto_div_atBot Real.instIsStrictOrderedRing instOrderTopologyReal
isBigOWith_of_tendsto_top 📖	mathematical	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Filter.atTop Real.instPreorder Real.instLT Real.instZero	Asymptotics.IsBigOWith Real Real.norm	—	Asymptotics.IsLittleO.forall_isBigOWith Asymptotics.IsLittleO.of_tendsto_div_atTop Real.instIsStrictOrderedRing instOrderTopologyReal
isBigO_of_div_tendsto_atBot 📖	mathematical	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Filter.atBot Real.instPreorder	Asymptotics.IsBigO Real Real.norm	—	Asymptotics.IsLittleO.isBigO Asymptotics.IsLittleO.of_tendsto_div_atBot Real.instIsStrictOrderedRing instOrderTopologyReal
isBigO_of_div_tendsto_atTop 📖	mathematical	Filter.Tendsto Real DivInvMonoid.toDiv Real.instDivInvMonoid Filter.atTop Real.instPreorder	Asymptotics.IsBigO Real Real.norm	—	Asymptotics.IsLittleO.isBigO Asymptotics.IsLittleO.of_tendsto_div_atTop Real.instIsStrictOrderedRing instOrderTopologyReal
tendsto_nhdsGT_of_tendsto_atTop 📖	mathematical	Filter.Tendsto Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	inv_atTop₀ Filter.map_add_left_nhdsGT IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing IsStrictOrderedRing.toIsTopologicalDivisionRing add_zero
tendsto_nhdsLT_of_tendsto_atTop 📖	mathematical	Filter.Tendsto SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	inv_atTop₀ Filter.neg_nhdsGT IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing IsStrictOrderedRing.toIsTopologicalDivisionRing neg_zero Filter.map_add_left_nhdsLT IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring add_zero AddGroupWithOne.sub_eq_add_neg
tendsto_nhdsNE_of_tendsto_atTop 📖	mathematical	Filter.Tendsto SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Filter.Tendsto nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	—	Filter.map_sup tendsto_nhdsLT_of_tendsto_atTop tendsto_nhdsGT_of_tendsto_atTop
tendsto_nhdsNE_of_tendsto_atTop_nhds_of_eq 📖	mathematical	Filter.Tendsto SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	Filter.Tendsto nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet nhds	—	tendsto_nhdsNE_of_tendsto_atTop

---

← Back to Index