Filter

📁 Source: Mathlib/Topology/Defs/Filter.lean

Statistics

Metric	Count
Definitions AccPt, CompactSpace, ContinuousAt, ContinuousWithinAt, coclosedCompact, cocompact, LocallyCompactPair, LocallyCompactSpace, MapClusterPt, NoncompactSpace, Specializes, nhdsGE, nhdsGT, nhdsLE, nhdsLT, nhdsNE, term𝓝, «term𝓝[_]_», «term𝓝ˢ[_]_», «term𝓝ˢ», WeaklyLocallyCompactSpace, inseparableSetoid, lim, limUnder, nhds, nhdsKer, nhdsSet, nhdsSetWithin, nhdsWithin, specializationPreorder, «term_⤳_»	31
Theorems isCompact_univ, exists_mem_nhds_isCompact_mapsTo, local_compact_nhds, noncompact_univ, exists_compact_mem_nhds, nhds_def	6
Total	37

CompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCompact_univ 📖	mathematical	—	IsCompact Set.univ	—	—

Filter

Definitions

Name	Category	Theorems
coclosedCompact 📖	CompOp	20 math math: OnePoint.continuous_iff, hasCompactSupport_iff_eventuallyEq, mem_coclosedCompact_iff, hasBasis_coclosedCompact, Homeomorph.comap_coclosedCompact, IsCompact.compl_mem_coclosedCompact_of_isClosed, OnePoint.comap_coe_nhds_infty, hasCompactMulSupport_iff_eventuallyEq, OnePoint.nhdsNE_infty_eq, compl_mem_coclosedCompact, coclosedCompact_eq_cocompact, OnePoint.continuousAt_infty', instNeBotCoclosedCompactOfNoncompactSpace, OnePoint.continuous_map_iff, cocompact_le_coclosedCompact, OnePoint.nhds_infty_eq, OnePoint.tendsto_nhds_infty', OnePoint.tendsto_coe_infty, coclosedCompact_le_cofinite, Homeomorph.map_coclosedCompact
cocompact 📖	CompOp	86 math math: comap_dist_left_atTop_eq_cocompact, tendsto_cocompact_mul_left, isProperMap_iff_tendsto_cocompact, coprodᵢ_cocompact, cocompact_le_atBot, isLittleO_exp_neg_mul_sq_cocompact, Metric.mem_cocompact_iff_closedBall_compl_subset, CocompactMap.cocompact_tendsto', IsClosed.tendsto_coe_cofinite_of_isDiscrete, Metric.mem_cocompact_of_closedBall_compl_subset, disjoint_cocompact_left, tendsto_cocompact_of_tendsto_dist_comp_atTop, disjoint_nhds_cocompact, Rat.not_countably_generated_cocompact, tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support, instIsMeasurablyGeneratedCocompactOfR1Space, cocompact_neBot_iff, Subgroup.tendsto_coe_cofinite_of_discrete, Homeomorph.comap_cocompact, cocompact_le_atTop, CocompactMap.tendsto_of_forall_preimage, IsCompact.compl_mem_cocompact, MeasureTheory.integrable_iff_integrableAtFilter_cocompact, AddSubgroup.tendsto_zmultiples_subtype_cofinite, cocompact_eq_atTop, tendsto_integral_exp_smul_cocompact, MonoidHom.tendsto_coe_cofinite_of_discrete, comap_cocompact_le, Complex.tendsto_normSq_cocompact_atTop, Metric.cobounded_le_cocompact, atBot_atTop_le_cocompact, Rat.cocompact_inf_nhds_neBot, Real.zero_at_infty_fourierIntegral, ZeroAtInftyContinuousMap.zero_at_infty', instNeBotCocompactOfNoncompactSpace, Homeomorph.map_cocompact, coprod_cocompact, tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact, tendsto_cocompact_cocompact_of_norm, isProperMap_iff_isClosedMap_and_tendsto_cofinite, ZeroAtInftyContinuousMapClass.zero_at_infty, tendsto_integral_exp_smul_cocompact_of_inner_product, CocompactMapClass.cocompact_tendsto, AddMonoidHom.tendsto_coe_cofinite_of_discrete, Int.tendsto_zmultiplesHom_cofinite, AddSubgroup.tendsto_coe_cofinite_of_discrete, cocompact_eq_atBot, SchwartzMap.tendsto_cocompact, Topology.IsClosedEmbedding.tendsto_cocompact, cexp_neg_quadratic_isLittleO_abs_rpow_cocompact, IsClosed.tendsto_coe_cofinite_of_discreteTopology, tendsto_dist_left_cocompact_atTop, cocompact_eq_atBot_atTop, HasCompactMulSupport.is_one_at_infty, tendsto_cofinite_cocompact_iff, tendsto_cocompact_mul_left₀, Real.zero_at_infty_fourier, tendsto_cocompact_mul_right₀, Metric.cobounded_eq_cocompact, coclosedCompact_eq_cocompact, Real.tendsto_integral_exp_smul_cocompact, tendsto_norm_cocompact_atTop', ModularGroup.tendsto_lcRow0, cocompact_le_cofinite, SchwartzMap.isBigO_cocompact_zpow_neg_nat, zero_at_infty_of_norm_le, tendsto_dist_right_cocompact_atTop, hasBasis_cocompact, cocompact_le_atBot_atTop, tendsto_integral_exp_inner_smul_cocompact, cocompact_eq_bot, disjoint_cocompact_right, cocompact_le_coclosedCompact, tendsto_cocompact_mul_right, IsClosed.tendsto_coe_cofinite_iff, HasCompactSupport.is_zero_at_infty, atTop_le_cocompact, cocompact_eq_cofinite, SchwartzMap.isBigO_cocompact_zpow, Int.tendsto_coe_cofinite, Real.zero_at_infty_vector_fourierIntegral, mem_cocompact', mem_cocompact, SchwartzMap.isBigO_cocompact_rpow, tendsto_norm_cocompact_atTop, atBot_le_cocompact

LocallyCompactPair

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mem_nhds_isCompact_mapsTo 📖	mathematical	Continuous Set Filter Filter.instMembership nhds	IsCompact Set.MapsTo	—	—

LocallyCompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
local_compact_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	Set.instHasSubset IsCompact	—	—

NoncompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
noncompact_univ 📖	mathematical	—	IsCompact Set.univ	—	—

Topology

Definitions

Name	Category	Theorems
nhdsGE 📖	CompOp	—
nhdsGT 📖	CompOp	—
nhdsLE 📖	CompOp	—
nhdsLT 📖	CompOp	—
nhdsNE 📖	CompOp	—
term𝓝 📖	CompOp	—
«term𝓝[_]_» 📖	CompOp	—
«term𝓝ˢ[_]_» 📖	CompOp	—
«term𝓝ˢ» 📖	CompOp	—

WeaklyLocallyCompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_compact_mem_nhds 📖	mathematical	—	IsCompact Set Filter Filter.instMembership nhds	—	—

(root)

Definitions

Name	Category	Theorems
AccPt 📖	MathDef	23 math math: AccPt.mono, accPt_sup, Set.Infinite.exists_accPt_of_subset_isCompact, uniqueDiffWithinAt_iff_accPt, Set.Infinite.exists_accPt_principal, accPt_principal_iff_nhdsWithin, AccPt.of_mem_tangentConeAt_ne_zero, mem_derivedSet, Set.Infinite.exists_accPt_cofinite_inf_principal, accPt_iff_nhds, Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact, MeasureTheory.exists_accPt_of_noAtoms, mem_codiscrete_accPt, accPt_iff_frequently_nhdsNE, Ordinal.accPt_subtype, mem_codiscreteWithin_accPt, accPt_iff_frequently, AccPt.nhds_inter, clusterPt_principal, UniqueDiffWithinAt.accPt, accPt_principal_iff_clusterPt, AccPt.map, accPt_iff_clusterPt
CompactSpace 📖	CompData	115 math math: Quotient.compactSpace, instCompactSpaceElemClosedBallOfProperSpace, compactSpace_generateFrom, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact, spectrum.instCompactSpace, compactSpace_generateFrom', ContinuousFunctionalCalculus.compactSpace_spectrum, ultrafilter_compact, Function.compactSpace, QuasispectrumRestricts.compactSpace, Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, CommRingCat.HomTopology.instCompactSpaceHomOfIsTopologicalRingOfT1SpaceOfCarrier, isCompact_iff_compactSpace, instCompactSpaceStoneCech, ArzelaAscoli.compactSpace_of_closed_inducing', Finite.compactSpace, SpectrumRestricts.compactSpace, TopologicalSpace.NonemptyCompacts.toCompactSpace, TopologicalSpace.vietoris.instCompactSpaceSet, AlgebraicGeometry.Scheme.compactSpace_of_isAffine, ArzelaAscoli.compactSpace_of_isClosedEmbedding, AlgebraicGeometry.isNoetherian_iff, Units.instCompactSpaceOfT1SpaceOfContinuousMul, AlgebraicGeometry.IsNoetherian.toCompactSpace, PadicInt.compactSpace, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1, AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace, TopologicalSpace.Compacts.instCompactSpace, AlgebraicGeometry.quasiCompact_over_affine_iff, ULift.compactSpace, instCompactSpaceAdditive, TopologicalSpace.Compacts.compactSpace_iff, DomAddAct.instCompactSpace, instCompactSpaceMultiplicative, Compactum.instCompactSpaceA, OnePoint.instCompactSpace, instCompactSpaceZerothHomotopy, GromovHausdorff.rep_gHSpace_compactSpace, Metric.sphere.compactSpace, AlgebraicGeometry.compactSpace_iff_quasiCompact, instCompactSpaceConnectedComponents, QuotientAddGroup.instCompactSpaceQuotientAddSubgroup, UniformSpace.compactSpace_iff_seqCompactSpace, TopologicalSpace.Compacts.instCompactSpaceSubtypeMem, Continuous.homeoOfEquivCompactToT2.t1_counterexample, AlgebraicGeometry.IsArtinianScheme.toCompactSpace, TopologicalSpace.Closeds.instCompactSpace, InfiniteGalois.instCompactSpaceAlgEquivOfIsGalois, Topology.IsClosedEmbedding.compactSpace, PrimeSpectrum.compactSpace, instCompactSpaceProd, IsNonarchimedeanLocalField.instCompactSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation, SingularManifold.instCompactSpaceM, AlgebraicGeometry.isArtinianScheme_iff, AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace, AlgebraicGeometry.compactSpace_iff_exists, Subsingleton.compactSpace, isCompact_univ_iff, SingularManifold.compactSpace, instCompactSpaceSum, CompHausLike.is_compact, Circle.instCompactSpace, Homeomorph.compactSpace, AddCircle.compactSpace, AddOpposite.instCompactSpace, ContinuousAddMonoidHom.instCompactSpace, TopologicalSpace.NonemptyCompacts.instCompactSpace, Valued.integer.properSpace_iff_compactSpace_integer, GromovHausdorff.compactSpace_optimalGHCoupling, Quot.compactSpace, UniformSpace.hausdorff.instCompactSpaceSet, not_compactSpace_iff, compactSpace_iff_seqCompactSpace, isProperMap_const_iff, ProfiniteGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux, Metric.compactSpace_iff_isBounded_univ, AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact, AlgebraicGeometry.Scheme.IsQuasiAffine.toCompactSpace, CompHaus.instCompactSpaceCarrierToTopTrue, SpectralSpace.toCompactSpace, instCompactSpaceProbabilityMeasure, ContinuousMonoidHom.instCompactSpace, AlgebraicGeometry.quasiCompact_iff_compactSpace, NonUnitalContinuousFunctionalCalculus.compactSpace_quasispectrum, TopologicalSpace.Closeds.compactSpace_iff, TopCat.instCompactSpaceCarrierDiskBoundary, TopologicalSpace.Fiber.instCompactSpaceElemValSetMemRangeCoeLocallyConstantPreimageSingleton, spectrum.instCompactSpaceNNReal, AlgebraicGeometry.compactSpace_of_universallyClosed, compactSpace_of_finite_subfamily_closed, compactSpace_of_completeLinearOrder, ClosedSubgroup.instCompactSpaceSubtypeMem, exists_compact_surjective_zorn_subset, compactSpace_Icc, Module.Finite.compactSpace, MulOpposite.instCompactSpace, TopologicalSpace.NonemptyCompacts.compactSpace_iff, CompHausLike.instCompactSpaceCarrierObjTopCatCompHausLikeToTop, AddUnits.instCompactSpaceOfT1SpaceOfContinuousAdd, ContinuousMap.instCompactSpaceElemCoeCompacts, DomMulAct.instCompactSpace, quasispectrum.instCompactSpaceNNReal, AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat, CategoryTheory.PreGaloisCategory.instCompactSpaceAutFunctorFintypeCat, WeakDual.CharacterSpace.instCompactSpaceElemCharacterSpaceOfProperSpace, TopologicalSpace.NoetherianSpace.compactSpace, stdSimplex.instCompactSpace_coe, instCompactSpaceQuotientIdeal, ProfiniteAddGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux, ClosedAddSubgroup.instCompactSpaceSubtypeMem, instCompactSpacePreStoneCech, QuotientGroup.instCompactSpaceQuotientSubgroup, quasispectrum.instCompactSpace, TopCat.instCompactSpaceCarrierDisk
ContinuousAt 📖	MathDef	246 math math: StrictMonoOn.continuousAt_of_exists_between, continuousAt_of_locally_lipschitz, EReal.continuousAt_add_coe_bot, continuousAt_const_cpow, EReal.continuousAt_add_coe_top, Monotone.continuousAt_iff_leftLim_eq_rightLim, Real.not_continuousAt_inv_log_neg_one, MDifferentiableAt.continuousAt, contMDiffAt_iff_of_mem_source, ContinuousOn.continuousAt_indicator, ConvexOn.continuousOn_tfae, continuousAt_toIocMod, Topology.IsInducing.continuousAt_iff, OpenPartialHomeomorph.continuousAt, continuousAt_zpow₀, EReal.continuousAt_add_coe_coe, ContinuousInv₀.continuousAt_inv₀, OnePoint.continuousAt_infty, not_continuousAt_of_tendsto, Real.continuousAt_tan, continuousAt_extChartAt, ContinuousOn.continuousAt_mulIndicator, intervalIntegral.continuousAt_of_dominated_interval, FiberBundle.continuousAt_totalSpace, Seminorm.continuousAt_zero_of_forall', IsOpen.continuousOn_iff, ContDiffAt.continuousAt_fderiv, Real.Angle.continuousAt_sign, EReal.continuousAt_add_bot_bot, continuousAt_of_monotoneOn_of_exists_between, continuousWithinAt_compl_self, SeparationQuotient.continuousAt_lift, continuousAt_subtype_val, Set.EquicontinuousAt.continuousAt_of_mem, HasGradientAt.continuousAt, AffineIsometryEquiv.continuousAt, mdifferentiableAt_iff, Metric.continuousAt_inv_infDist_pt, Filter.EventuallyEq.continuousAt, continuousWithinAt_univ, OpenPartialHomeomorph.continuousAt_extend_symm', Real.not_continuousAt_deriv_mul_log_zero, continuousAt_iff_ultrafilter, Complex.continuousAt_arg, continuousAt_toIocDiv, continuousAt_of_monotoneOn_of_closure_image_mem_nhds, IsDenseInducing.continuousAt_extend, Filter.Tendsto.continuousAt_of_equicontinuousAt, continuousAt_inv, upperHemicontinuousAt_singleton_iff, Real.continuousAt_rpow_const, UniformSpace.Completion.continuous_hatInv, Real.continuousAt_rpow_of_pos, Complex.continuousAt_cpow_const_of_re_pos, Real.continuousAt_const_rpow', ENNReal.continuousAt_mul_const, IsGδ.setOf_continuousAt, List.Vector.continuousAt_eraseIdx, continuousAt_dslope_same, DifferentiableAt.continuousAt, Topology.IsOpenEmbedding.continuousAt_iff, continuousAt_cpow, OpenPartialHomeomorph.continuousAt_extend, continuousAt_neg, continuousAt_const_vadd_iff, Monotone.countable_not_continuousAt, Complex.continuousAt_Gamma_one, continuousAt_congr, Homeomorph.comp_continuousAt_iff', ENNReal.continuousAt_const_mul, Seminorm.continuousAt_zero', ChartedSpace.liftPropAt_iff, IsCoveringMapOn.continuousAt, NNReal.continuousAt_rpow, continuousAt_toIcoMod, Oscillation.eq_zero_iff_continuousAt, Complex.not_continuousAt_Gamma_zero, Real.continuousAt_logb_iff, ENat.continuousAt_sub, continuousAt_iff_continuous_left'_right', contMDiffAt_iff, IsLocalHomeomorphOn.continuousAt, continuousAt_clog, EReal.continuousAt_add_bot_coe, OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_right, Antitone.countable_not_continuousAt, continuousAt_const, Asymptotics.continuousAt_iff_isLittleO, MeromorphicAt.eventually_continuousAt, continuousAt_const_smul_iff₀, ContMDiffAt.continuousAt, CPolynomialAt.continuousAt, Antitone.continuousAt_iff_leftLim_eq_rightLim, continuousWithinAt_iff_continuousAt, Real.continuousAt_arcsin, continuousAt_iff_continuous_left_right, IsMIntegralCurveAt.continuousAt, ENNReal.continuousAt_toReal, continuousAt_fract, NormedField.continuousAt_inv, Uniform.continuousAt_iff'_left, continuousAt_prod_of_discrete_right, Complex.differentiableOn_compl_singleton_and_continuousAt_iff, Orientation.continuousAt_oangle, SeparationQuotient.continuousAt_lift₂, Metric.continuousAt_iff', Complex.continuousAt_ofReal_cpow, EuclideanGeometry.continuousAt_angle, continuousAt_gauge_zero, continuousAt_gauge, Real.continuousAt_rpow_of_ne, UniformOnFun.continuousOn_eval₂, Complex.continuousAt_cpow_zero_of_re_pos, Continuous.continuousAt, EuclideanGeometry.continuousAt_oangle, HasStrictFDerivAt.localInverse_continuousAt, mdifferentiableAt_iff_target_of_mem_source, Complex.continuousAt_arg_coe_angle, HasDerivAt.continuousAt, continuousAt_extChartAt_symm, contMDiffAt_iff_target_of_mem_source, continuousAt_zpow, continuousAt_const_cpow', NormedField.continuousAt_zpow, continuousAt_of_monotoneOn_of_image_mem_nhds, NNReal.continuousAt_rpow_const, continuousAt_iff_punctured_nhds, ModelWithCorners.continuousAt, StrictMonoOn.continuousAt_of_image_mem_nhds, continuousAt_pi, Topology.IsInducing.continuousAt_iff', StrictMonoOn.continuousAt_of_closure_image_mem_nhds, Real.smoothTransition.continuousAt, EReal.continuousAt_add_top_coe, continuousAt_cpow_const, ENNReal.continuousAt_coe_iff, map_continuousAt, OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left, continuousAt_of_not_accPt_top, Real.continuousAt_log_iff, continuousAt_jacobiTheta, Seminorm.continuousAt_zero_of_forall, EquicontinuousAt.continuousAt, continuousAt_codRestrict_iff, LinearIsometryEquiv.continuousAt, continuousAt_extChartAt', continuousAt_toIcoDiv, OnePoint.continuousAt_infty', continuousAt_jacobiTheta₂, continuousAt_update_of_ne, measurableSet_of_continuousAt, Complex.not_continuousAt_Gamma_neg_nat, Real.not_continuousAt_deriv_qaryEntropy_zero, Trivialization.continuousAt_proj, continuousAt_sign_of_neg, continuousAt_prod_of_discrete_left, AddCircle.continuousAt_equivIoc, Real.continuousAt_const_rpow, continuousAt_zsmul, ContinuousLinearEquiv.continuousAt, continuousAt_neg_iff, PeriodPair.not_continuousAt_weierstrassP, mdifferentiableAt_iff_of_mem_source, Uniform.continuousAt_iff'_right, AddCircle.continuousAt_equivIco, continuousAt_sign_of_pos, continuousAt_star, HasDerivAt.continuousAt_div, OpenPartialHomeomorph.continuousAt_extend_symm, EReal.continuousAt_add, continuousAt_nsmul, continuousAt_apply, Homeomorph.comp_continuousAt_iff, continuousWithinAt_iff_continuousAt_restrict, NormedRing.inverse_continuousAt, continuousAt_hom_bundle, AnalyticAt.continuousAt, Real.continuousAt_rpow, EReal.continuousAt_add_top_top, continuousAt_id', continuousAt_of_not_accPt, continuousAt_jacobiTheta₂', ConcaveOn.continuousOn_tfae, Polynomial.continuousAt, ModelWithCorners.continuousAt_symm, continuousAt_inv_iff, HasMFDerivAt.continuousAt, equicontinuousAt_iff_continuousAt, Real.continuousAt_logb, IsUnit.continuousAt_const_smul_iff, continuousAt_of_tendsto_nhds, mdifferentiableAt_iff_target, Metric.continuousAt_iff, Real.not_continuousAt_inv_log_one, ContDiffAt.continuousAt, HasFDerivAt.continuousAt, Complex.continuousAt_cpow_of_re_pos, ContDiffAt.continuousAt_iteratedFDeriv, HasFPowerSeriesAt.continuousAt, Complex.continuousAt_Gamma, continuousAt_def, continuousAt_extChartAt_symm'', Real.continuousAt_log, OnePoint.continuousAt_coe, IsEvenlyCovered.continuousAt, HasFiniteFPowerSeriesAt.continuousAt, OpenPartialHomeomorph.continuousAt_symm, ContinuousAlgEquiv.continuousAt, ContinuousOn.continuousAt, ContinuousWithinAt.continuousAt, EReal.continuousAt_mul, InnerProductGeometry.continuousAt_angle, Real.continuousAt_arctan, Real.not_continuousAt_deriv_qaryEntropy_one, continuousAt_snd, IsOpenQuotientMap.continuousAt_comp_iff, Bundle.RiemannianMetric.continuousAt, contMDiffAt_iff_target, continuousAt_sign_of_ne_zero, List.continuousAt_length, equicontinuousAt_finite, ContinuousMap.continuousAt, continuousAt_id, HasStrictFDerivAt.continuousAt, continuousAt_extChartAt_symm', continuousAt_fst, Polynomial.continuousAt_aeval, equicontinuousAt_unique, continuousAt_update_same, Complex.continuousAt_ofReal_cpow_const, continuousAt_gaussian_integral, Seminorm.continuousAt_zero, continuous_iff_continuousAt, Complex.continuousAt_tan, Uniform.continuousAt_iff_prod, Dense.continuousAt_extend, continuousAt_iff_lower_upperSemicontinuousAt, AnalyticAt.eventually_continuousAt, ContinuousLinearMap.continuousAt_uncurry_of_multilinear, continuousAt_cfc_fun, LinearMap.continuousAt_zero_of_locally_bounded, continuousAt_cfcₙ_fun, ContDiffPointwiseHolderAt.continuousAt, continuousAt_const_smul_iff, continuousAt_pow, continuousAt_dslope_of_ne
ContinuousWithinAt 📖	MathDef	179 math math: StrictMonoOn.continuousWithinAt_right_of_image_mem_nhdsWithin, MonotoneOn.countable_not_continuousWithinAt_Ioi, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart', StrictMonoOn.continuousWithinAt_right_of_closure_image_mem_nhdsWithin, contMDiffWithinAt_iff_target, Metric.continuousWithinAt_iff', continuousWithinAt_diff_self, Complex.continuousWithinAt_arg_of_re_neg_of_im_zero, mdifferentiableWithinAt_iff_of_mem_maximalAtlas, AntitoneOn.countable_not_continuousWithinAt, ModelWithCorners.symm_continuousWithinAt_comp_right_iff, continuousWithinAt_Icc_iff_Ici, continuousWithinAt_Ico_iff_Ici, continuousWithinAt_inter_Ioi_iff_Ici, continuousWithinAt_Icc_iff_Iic, mdifferentiableWithinAt_iff_target_inter, contMDiffWithinAt_iff_image, Complex.continuousWithinAt_log_of_re_neg_of_im_zero, continuousWithinAt_prod_of_discrete_left, StrictMonoOn.continuousWithinAt_right_of_surjOn, continuousWithinAt_compl_self, ChartedSpace.LiftPropWithinAt.continuousWithinAt, continuous_right_toIcoMod, FiberBundle.continuousWithinAt_totalSpace, Filter.EventuallyEq.congr_continuousWithinAt_of_mem, continuousWithinAt_univ, continuousWithinAt_toIcoMod_Ici, Polynomial.continuousWithinAt, HasGradientWithinAt.continuousWithinAt, continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin, ContDiffWithinAt.continuousWithinAt_iteratedFDerivWithin, AffineIsometryEquiv.continuousWithinAt, continuousWithinAt_Ico_iff_Iio, continuous_left_toIocMod, ContinuousAt.continuousWithinAt, equicontinuousWithinAt_iff_continuousWithinAt, continuousWithinAt_union, continuousWithinAt_Ioc_iff_Ioi, continuousWithinAt_iff_lower_upperSemicontinuousWithinAt, LeftOrdContinuous.continuousWithinAt_Iic, Set.EquicontinuousWithinAt.continuousWithinAt_of_mem, continuousWithinAt_right_of_monotoneOn_of_image_mem_nhdsWithin, continuousWithinAt_of_notMem_closure, SeparationQuotient.continuousWithinAt_lift, continuousWithinAt_dslope_of_ne, map_continuousWithinAt, AnalyticWithinAt.continuousWithinAt, continuousWithinAt_insert, Homeomorph.comp_continuousWithinAt_iff, EquicontinuousWithinAt.continuousWithinAt, StrictMonoOn.continuousWithinAt_left_of_image_mem_nhdsWithin, Uniform.continuousWithinAt_iff'_right, OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff, continuousWithinAt_Ioo_iff_Iio, StrictMonoOn.continuousWithinAt_left_of_exists_between, ContinuousAlgEquiv.continuousWithinAt, continuousWithinAt_prod_of_discrete_right, continuousWithinAt_insert_self, continuousWithinAt_right_of_monotoneOn_of_exists_between, continuousWithinAt_id, continuousWithinAt_iff_continuous_left'_right', intervalIntegral.continuousWithinAt_of_dominated_interval, contMDiffWithinAt_iff_of_mem_source', mdifferentiableWithinAt_iff_image, ContDiffWithinAt.continuousWithinAt_fderivWithin, StrictMonoOn.continuousWithinAt_right_of_exists_between, continuousAt_iff_continuous_left'_right', Uniform.continuousWithinAt_iff'_left, OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right, LinearIsometryEquiv.continuousWithinAt, continuousWithinAt_inter_Iio_iff_Iic, continuousWithinAt_const_smul_iff, continuousWithinAt_neg, ModelWithCorners.continuousWithinAt, continuousWithinAt_const_smul_iff₀, continuousWithinAt_diff_singleton, contMDiffWithinAt_iff_target_of_mem_source, ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear, StructureGroupoid.liftPropWithinAt_self_target, continuousWithinAt_iff_continuousAt, continuousAt_iff_continuous_left_right, Monotone.continuousWithinAt_Iio_iff_leftLim_eq, continuousWithinAt_const_vadd_iff, contMDiffWithinAt_iff, MonotoneOn.countable_not_continuousWithinAt, Monotone.continuousWithinAt_Ioi_iff_rightLim_eq, continuousWithinAt_cfc_fun, intervalIntegral.continuousWithinAt_primitive, Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt, Metric.continuousWithinAt_iff, Antitone.continuousWithinAt_Iio_iff_leftLim_eq, mdifferentiableWithinAt_iff', AnalyticWithinAt.continuousWithinAt_insert, continuousWithinAt_singleton, StructureGroupoid.liftPropWithinAt_self, Filter.EventuallyEq.congr_continuousWithinAt, continuousWithinAt_congr_set, contMDiffWithinAt_iff', HasMFDerivWithinAt.continuousWithinAt, equicontinuousWithinAt_unique, ModelWithCorners.continuousWithinAt_symm, mdifferentiableWithinAt_iff_target_inter', DifferentiableWithinAt.continuousWithinAt, continuousWithinAt_left_of_monotoneOn_of_image_mem_nhdsWithin, HasFPowerSeriesWithinAt.continuousWithinAt_insert, ContDiffWithinAt.continuousWithinAt, continuousWithinAt_iff_ptendsto_res, continuousWithinAt_toIocDiv_Iic, mdifferentiableWithinAt_iff_of_mem_source', continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin, ProbabilityTheory.IsMeasurableRatCDF.continuousWithinAt_stieltjesFunctionAux_Ici, mdifferentiableWithinAt_iff, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff, IsMIntegralCurveOn.continuousWithinAt, continuousWithinAt_Ioo_iff_Ioi, OpenPartialHomeomorph.extend_symm_continuousWithinAt_comp_right_iff, equicontinuousWithinAt_finite, HasFPowerSeriesWithinAt.continuousWithinAt, contMDiffWithinAt_iff_of_mem_maximalAtlas, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target, StrictMonoOn.continuousWithinAt_left_of_closure_image_mem_nhdsWithin, continuousWithinAt_cfcₙ_fun, continuousWithinAt_snd, RightOrdContinuous.continuousWithinAt_Ici, continuousWithinAt_Ioc_iff_Iic, continuousWithinAt_pi, continuousWithinAt_rightLim_Ici, mdifferentiableWithinAt_iff_target_of_mem_source, continuousWithinAt_iff_continuousAt_restrict, SeparationQuotient.continuousWithinAt_lift₂, continuousWithinAt_congr, ContMDiffWithinAt.continuousWithinAt, continuousWithinAt_inter', continuousWithinAt_hom_bundle, continuousWithinAt_prod_iff, HasFPowerSeriesWithinOnBall.continuousWithinAt_insert, HasFDerivWithinAt.continuousWithinAt, continuousWithinAt_inv, continuousWithinAt_Iio_iff_Iic, continuousWithinAt_const, continuousWithinAt_update_of_ne, StructureGroupoid.liftPropWithinAt_self_source, continuousWithinAt_inter, HasDerivWithinAt.continuousWithinAt, continuousWithinAt_toIocMod_Iic, upperHemicontinuousWithinAt_singleton_iff, continuousWithinAt_update_same, mdifferentiableWithinAt_iff_of_mem_source, continuousWithinAt_fst, Continuous.continuousWithinAt, OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left, MonotoneOn.countable_not_continuousWithinAt_Iio, continuousWithinAt_leftLim_Iic, continuousWithinAt_toIcoDiv_Ici, MDifferentiableWithinAt.continuousWithinAt, StrictMonoOn.continuousWithinAt_left_of_surjOn, continuousWithinAt_iff_continuous_left_right, Filter.EventuallyEq.congr_continuousWithinAt_of_insert, continuousWithinAt_congr_of_insert, continuousWithinAt_congr_set', Topology.IsInducing.continuousWithinAt_iff, continuousWithinAt_left_of_monotoneOn_of_exists_between, continuousWithinAt_of_not_accPt, StieltjesFunction.right_continuous, ContinuousLinearEquiv.continuousWithinAt, continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_congr_of_mem, OscillationWithin.eq_zero_iff_continuousWithinAt, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart, mdifferentiableWithinAt_iff_target, HasFPowerSeriesWithinOnBall.continuousWithinAt, continuousWithinAt_star, contMDiffWithinAt_iff_of_mem_source, Antitone.continuousWithinAt_Ioi_iff_rightLim_eq, ContinuousOn.continuousWithinAt, IsUnit.continuousWithinAt_const_smul_iff, Polynomial.continuousWithinAt_aeval, ChartedSpace.liftPropWithinAt_iff', StieltjesFunction.right_continuous'
LocallyCompactPair 📖	CompData	2 math math: instLocallyCompactPairOfLocallyCompactSpace, instLocallyCompactPairOfWeaklyLocallyCompactSpaceOfR1Space
LocallyCompactSpace 📖	CompData	51 math math: IsNonarchimedeanLocalField.toLocallyCompactSpace, locallyCompact_of_proper, ModelWithCorners.locallyCompactSpace, Function.locallyCompactSpace, ContinuousAddMonoidHom.locallyCompactSpace_of_hasBasis, Manifold.locallyCompact_of_finiteDimensional, RestrictedProduct.instLocallyCompactSpaceCoeCofiniteOfSubgroupClassOfIsTopologicalGroupOfCompactSpaceSubtypeMem, instLocallyCompactSpacePontryaginDual, HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group, AbsoluteValue.Completion.locallyCompactSpace, ContinuousMonoidHom.locallyCompactSpace_of_equicontinuousAt, NumberField.InfinitePlace.Completion.locallyCompactSpace, ChartedSpace.locallyCompactSpace, Units.instLocallyCompactSpaceOfT1SpaceOfContinuousMul, Function.locallyCompactSpace_of_finite, MulOpposite.instLocallyCompactSpace, IsLocallyClosed.locallyCompactSpace, WeaklyLocallyCompactSpace.locallyCompactSpace, DomAddAct.instLocallyCompactSpace, Topology.IsOpenEmbedding.locallyCompactSpace, IsOpenQuotientMap.locallyCompactSpace, IsOpen.locallyCompactSpace, instLocallyCompactSpaceMultiplicative, IsClosed.locallyCompactSpace, IsCompact.locallyCompactSpace_of_mem_nhds_of_group, instLocallyCompactSpaceAdditive, Homeomorph.locallyCompactSpace_iff, UpperHalfPlane.instLocallyCompactSpace, eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_addGroup, QuotientAddGroup.instLocallyCompactSpace, Prod.locallyCompactSpace, NumberField.InfiniteAdeleRing.locallyCompactSpace, LocallyCompactSpace.of_finiteDimensional_of_complete, instLocallyCompactSpaceOfPrespectralSpace, LocallyCompactSpace.of_hasBasis, AlexandrovDiscrete.toLocallyCompactSpace, RestrictedProduct.instLocallyCompactSpaceCoeCofiniteOfAddSubgroupClassOfIsTopologicalAddGroupOfCompactSpaceSubtypeMem, eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group, ContinuousMonoidHom.locallyCompactSpace_of_hasBasis, TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_group, IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup, Topology.IsInducing.locallyCompactSpace, LocallyCompactSpace.of_locallyCompact_manifold, AddUnits.instLocallyCompactSpaceOfT1SpaceOfContinuousAdd, QuotientGroup.instLocallyCompactSpace, TopologicalSpace.PositiveCompacts.locallyCompactSpace_of_addGroup, Topology.IsClosedEmbedding.locallyCompactSpace, DomMulAct.instLocallyCompactSpace, HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup, ContinuousAddMonoidHom.locallyCompactSpace_of_equicontinuousAt, AddOpposite.instLocallyCompactSpace
MapClusterPt 📖	MathDef	39 math math: mapClusterPt_atTop_pow_tfae, Filter.Tendsto.mapClusterPt, mapClusterPt_leftLim, mapClusterPt_id_iff, mapClusterPt_def, mapClusterPt_neg_atTop_nsmul, MapClusterPt.tendsto_comp', MapClusterPt.prodMap, mapClusterPt_atTop_nsmul_tfae, mapClusterPt_iff_ultrafilter, IsCompact.exists_mapClusterPt, mapClusterPt_self_zsmul_atTop_nsmul, mapClusterPt_atTop_zsmul_iff_nsmul, mapClusterPt_self_atTop_pow, ClusterPt.mapClusterPt_id, mapClusterPt_one_atTop_pow, mapClusterPt_rightLim, mapClusterPt_self_zpow_atTop_pow, mapClusterPt_zero_atTop_nsmul, mapClusterPt_atTop_zpow_iff_pow, mapClusterPt_self_atTop_nsmul, mapClusterPt_iff_frequently, MapClusterPt.mono, MapClusterPt.tendsto_comp, MapClusterPt.continuousAt_comp, ContinuousAt.mapClusterPt, IsCompact.exists_mapClusterPt_of_frequently, mapClusterPt_atTop_pow_iff_mem_topologicalClosure_zpowers, MapClusterPt.curry_prodMap, MapClusterPt.congrFun, MapClusterPt.of_comp, Filter.HasBasis.mapClusterPt_iff_frequently, mapClusterPt_comp, Topology.IsInducing.mapClusterPt_iff, mapClusterPt_atTop_nsmul_iff_mem_topologicalClosure_zmultiples, Filter.EventuallyEq.mapClusterPt_iff, mapClusterPt_inv_atTop_pow, IsClosedMap.mapClusterPt_iff_lift'_closure, mem_omegaLimit_singleton_iff_map_cluster_point
NoncompactSpace 📖	CompData	25 math math: TopologicalSpace.Closeds.noncompactSpace_iff, RealNormedSpace.noncompactSpace, Filter.cocompact_neBot_iff, Topology.IsClosedEmbedding.noncompactSpace, TopologicalSpace.Closeds.instNoncompactSpace, Nat.instNoncompactSpace, UpperHalfPlane.instNoncompactSpace, Prod.noncompactSpace_iff, instNoncompactSpaceInt, Prod.noncompactSpace_left, instNoncompactSpaceAdditive, instNoncompactSpaceMultiplicative, Prod.noncompactSpace_right, instNoncompactSpaceReal, TopologicalSpace.Compacts.instNoncompactSpace, TopologicalSpace.Compacts.noncompactSpace_iff, not_compactSpace_iff, TopologicalSpace.NonemptyCompacts.noncompactSpace_iff, Rat.instNoncompactSpace, NormedSpace.noncompactSpace, TopologicalSpace.NonemptyCompacts.instNoncompactSpace, PNat.instNoncompactSpace, Metric.ediam_univ_eq_top_iff_noncompact, noncompactSpace_of_neBot, NormedField.noncompactSpace
Specializes 📖	MathDef	63 math math: IsGenericPoint.specializes_iff_mem, TopologicalSpace.vietoris.specializes_of_subset_closure, isClosed_setOf_specializes, R0Space.specializes_symmetric, Topology.IsInducing.specializes_iff, TopologicalSpace.vietoris.specializes_closure, ContinuousMap.specializes_coe, Inseparable.specializes', inseparable_iff_specializes_and, IsGenericPoint.specializes, AlgebraicGeometry.Scheme.range_fromSpecStalk, mem_nhdsKer_iff_specializes, disjoint_nhds_nhds_iff_not_specializes, Topology.WithUpperSet.toUpperSet_specializes_toUpperSet, specializes_iff_mem_closure, ker_nhds_eq_specializes, not_specializes_iff_exists_open, isGenericPoint_iff_specializes, Specialization.toEquiv_le_toEquiv, Specializes.of_eq, IsLocalRing.specializes_closedPoint, not_specializes_iff_exists_closed, OnePoint.not_specializes_infty_coe, specializes_iff_nhdsKer_subset, R1Space.specializes_or_disjoint_nhds, Topology.WithUpperSet.ofUpperSet_le_ofUpperSet, PrimeSpectrum.le_iff_specializes, Inseparable.specializes, specializes_eq_eq, specializes_prod, specializes_iff_eq, Topology.IsLowerSet.specializes_iff_le, specializes_rfl, r0Space_iff, genericPoint_specializes, specializes_iff_clusterPt, specializes_iff_nhds, IsClosed.not_specializes, specializes_of_nhdsWithin, subtype_specializes_iff, specializes_iff_not_disjoint, specializes_iff_pure, OnePoint.specializes_coe, specializes_iff_inseparable, Topology.WithLowerSet.ofLowerSet_le_ofLowerSet, specializes_iff_forall_closed, Specialization.ofEquiv_specializes_ofEquiv, specializes_iff_forall_open, r1Space_iff_specializes_or_disjoint_nhds, specializes_comm, mem_nhdsKer_singleton, IsOpen.not_specializes, specializes_iff_closure_subset, specializes_refl, Filter.HasBasis.specializes_iff_uniformity, Filter.HasBasis.specializes_iff, AlgebraicGeometry.Scheme.le_iff_specializes, Topology.IsUpperSet.specializes_iff_le, specializes_TFAE, Filter.specializes_iff_le, specializes_pi, Topology.WithLowerSet.toLowerSet_specializes_toLowerSet, specializes_of_eq
WeaklyLocallyCompactSpace 📖	CompData	14 math math: instWeaklyLocallyCompactSpaceOfLocallyCompactSpace, instWeaklyLocallyCompactSpaceMultiplicative, AddUnits.instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousAdd, DomMulAct.instWeaklyLocallyCompactSpace, IsOpenQuotientMap.weaklyLocallyCompactSpace, Units.instWeaklyLocallyCompactSpaceOfT1SpaceOfContinuousMul, instWeaklyLocallyCompactSpaceProd, AddOpposite.instWeaklyLocallyCompactSpace, Topology.IsClosedEmbedding.weaklyLocallyCompactSpace, MulOpposite.instWeaklyLocallyCompactSpace, instWeaklyLocallyCompactSpaceOfCompactSpace, instWeaklyLocallyCompactSpaceAdditive, IsClosed.weaklyLocallyCompactSpace, DomAddAct.instWeaklyLocallyCompactSpace
inseparableSetoid 📖	CompOp	2 math math: SeparationQuotient.inseparableSetoid_eq_top_iff, UniformSpace.inseparableSetoid_ring
lim 📖	CompOp	8 math math: lim_eq, CauchyFilter.cauchyFilter_eq, Cauchy.le_nhds_lim, lim_nhdsWithin, le_nhds_lim, lim_eq_iff, CauchyFilter.inseparable_lim_iff, lim_nhds
limUnder 📖	CompOp	17 math math: limUnder_nhds_id, Function.Periodic.cuspFunction_zero_eq_limUnder_nhds_ne, Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_bounded_under, Complex.differentiableOn_update_limUnder_of_isLittleO, Complex.differentiableOn_update_limUnder_of_bddAbove, Continuous.limUnder_eq, limUnder_of_not_tendsto, Filter.limUnder_eq_iff, CauchySeq.tendsto_limUnder, tendsto_nhds_limUnder, Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO, MeasureTheory.StronglyMeasurable.limUnder, Complex.differentiableOn_update_limUnder_insert_of_isLittleO, MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi, limUnder_nhdsWithin_id, Filter.Tendsto.limUnder_eq, MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic
nhds 📖	CompOp	2213 math math: SuccOrder.hasBasis_nhds_Ioc, withSeminorms_iff_mem_nhds_isVonNBounded, pi_Iio_mem_nhds, MeasureTheory.tendstoInMeasure_iff_measureReal_norm, Filter.IsApproximateUnit.iff_le_nhds_one, HasStrictFDerivAt.isBigO_sub, Metric.equicontinuousAt_iff_right, EReal.nhds_top_basis, IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto, HasStrictFDerivAt.map_implicitFunctionOfComplemented_eq, NNReal.tendsto_agmSequences_fst_agm, nhds_hasBasis_absConvex_open, ENNReal.nhds_zero, nhds_basis_one_mabs_lt, tendsto_zero_iff_meromorphicOrderAt_pos, MvPowerSeries.WithPiTopology.tendsto_trunc_atTop, Filter.tendsto_nhds_atBot_iff, HasStrictFDerivAt.isLittleOTVS, ProbabilityTheory.tendsto_defaultRatCDF_atBot, Function.LeftInverse.map_nhds_eq, Metric.closedEBall_mem_nhds, MonoidHom.exists_nhds_isBounded, mem_nhds_discrete, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm'', ProbabilityTheory.Kernel.tendsto_m_density, OpenPartialHomeomorph.extend_source_mem_nhds, IsOpen.nhdsWithin_eq, upperHemicontinuousAt_iff_forall_isOpen, Filter.nhds_atBot, Complex.tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero, nhdsSet_insert, Topology.IsOpenEmbedding.map_nhds_eq, IsLocalDiffeomorphAt.localInverse_eventuallyEq_right, IsDiscrete.exists_nhds_eq_zero_of_image_addLeft_inter_nonempty, IsTopologicalAddGroup.isInducing_iff_nhds_zero, Real.map_exp_nhds, NormedCommGroup.tendsto_nhds_nhds, OpenPartialHomeomorph.symm_map_nhds_eq, toIcoMod_eventuallyEq_toIocMod, MeasureTheory.Measure.finiteAt_nhds, Filter.IsApproximateUnit.tendsto_mul_left, nhds_neBot, comap_gauge_nhds_zero_le, GroupFilterBasis.nhds_hasBasis, eventually_nhds_nhdsWithin, Filter.nhds_eq', tendsto_birkhoffAverage_apply_sub_birkhoffAverage', BumpCovering.eventuallyEq_one, Dilation.tendsto_nhds_iff, Ctop.mem_nhds_toTopsp, Filter.HasBasis.clusterPt_iff_frequently', gt_mem_nhds, tendsto_inv_atTop_zero, Bornology.isVonNBounded_iff_tendsto_smallSets_nhds, tendsto_const_mul_pow_nhds_iff', le_nhds_iff_adhp_of_cauchy, tendsto_smoothingFun_of_ne_zero, NormedRing.inverse_one_sub_norm, IsUltraUniformity.mem_nhds_iff_symm_trans, nhds_ofMul, map_mul_left_nhds, nhds_bot_basis, limUnder_nhds_id, nhds_sInf, ConvexOn.continuousOn_tfae, tendsto_tsum_div_pow_atTop_integral, ContinuousAlgEquiv.map_nhds_eq, ProbabilityTheory.tendsto_defaultRatCDF_atTop, compact_open_separated_add_right, RCLike.tendsto_inverse_atTop_nhds_zero_nat, hasSum_iff_tendsto_nat_of_summable_norm, Ultrafilter.clusterPt_iff, ContinuousMap.hasBasis_nhds, IsUniformAddGroup.cauchy_map_iff_tendsto, map_mul_right_nhds_one, GenContFract.of_convergence, tendsto_ceil_right', SeminormFamily.basisSets_smul_right, OpenPartialHomeomorph.eventually_left_inverse', tendsto_atBot_of_antitone, OnePoint.continuous_iff, SupConvergenceClass.tendsto_coe_atTop_isLUB, tendsto_const_div_atTop_nhds_zero_nat, ContinuousLinearMapWOT.le_nhds_iff_forall_inner_apply_le_nhds, Continuous.tendsto_nhdsSet_nhds, UpperHemicontinuous.forall_isOpen, OpenPartialHomeomorph.map_extend_nhds_of_boundaryless, AkraBazziRecurrence.tendsto_zero_sumCoeffsExp, Absorbs.eventually_nhds_zero, prod_nhds_le_of_disjoint_cocompact, Real.rpow_eq_nhds_of_neg, le_nhdsAdjoint_iff, SeparationQuotient.tendsto_lift_nhds_mk, CFC.tendsto_cfc_rpow_sub_one_log, Topology.IsInducing.nhds_eq_comap, Ioi_mem_nhds, MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_eLpNorm, nhds_le_nhdsSet, ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendsto, TrivSqZeroExt.nhds_def, isProperMap_iff_ultrafilter, SeminormedGroup.disjoint_nhds, Asymptotics.isLittleOTVS_one, HasStrictFDerivAt.map_nhds_eq_of_equiv, Asymptotics.isLittleO_const_iff, Polynomial.div_tendsto_atTop_leadingCoeff_div_of_degree_eq, Complex.GammaSeq_tendsto_Gamma, WithIdealFilter.mem_nhds_zero_iff, Function.Periodic.tendsto_nhds_zero, mem_nhds_prod_iff, LinearOrderedCommGroup.tendsto_nhds, EquicontinuousOn.tendsto_uniformOnFun_iff_pi', nhds_vadd, MeasureTheory.StronglyMeasurable.tendsto_approxBounded_ae, map_mul_left_nhds_one₀, IsUniformAddGroup.ext_iff, nhds_eq_nhds_iff, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_one_of_monotone, chart_target_mem_nhds, AddGroupFilterBasis.nhds_hasBasis, NormedCommGroup.nhds_one_basis_norm_lt, WithSeminorms.mem_nhds_iff, nhds_iInf, locallyFinite_iff_smallSets, comap_conj_nhds_zero, AntitoneOn.tendsto_nhdsGT, Antitone.tendsto_rightLim, Polynomial.div_tendsto_atBot_leadingCoeff_div_of_degree_eq, Units.nhds, UniformSpace.ball_mem_nhds, ContDiffBump.eventuallyEq_one, QuotientGroup.nhds_eq, MeasureTheory.measurableSet_exists_tendsto, uniformity_eq_comap_add_neg_nhds_zero, ProbabilityTheory.tendsto_condCDF_atBot, MeasureTheory.UniformIntegrable.uniformIntegrable_of_ae_tendsto, MeasureTheory.tendsto_Lp_of_tendstoInMeasure, subset_interior_iff_nhds, MeasureTheory.isTightMeasureSet_iff_inner_tendsto, GroupFilterBasis.nhds_one_eq, MeasureTheory.ProbabilityMeasure.toMeasure_add_pos_gt_mem_nhds, TopologicalSpace.Opens.chartAt_subtype_val_symm_eventuallyEq, Metric.equicontinuousAt_iff_pair, exists_seq_strictAnti_tendsto', MeasureTheory.piContent_tendsto_zero, tendsto_inv_iff, isQuotientCoveringMap_iff, tendsto_one_iff_mabs_tendsto_one, tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero, extChartAt_target_eventuallyEq, nhds_mul_nhds_one, Metric.nhds_basis_closedBall_pow, SeminormFamily.filter_eq_iInf, ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq, Metric.eventually_prod_nhds_iff, DomAddAct.map_mk_symm_nhds, Metric.tendsto_atTop, ENNReal.tendsto_nat_tsum, MeasureTheory.tendsto_measure_iUnion_atBot, Iio_mem_nhds, OpenPartialHomeomorph.extend_preimage_mem_nhds_of_mem_nhdsWithin, NormedRing.inverse_add_norm_diff_nth_order, Equicontinuous.isClosed_setOf_tendsto, WithZeroTopology.nhds_zero, eventually_homothety_image_subset_of_finite_subset_interior, IsClosedMap.comap_nhds_eq, pi_Ioo_mem_nhds, ContDiffPointwiseHolderAt.isBigO, Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_bounded_under, CircleDeg1Lift.tendsto_translationNumber_aux, tendsto_cfc_fun, Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet, cauchySeq_iff_tendsto_dist_atTop_0, IsDenseInducing.nhds_eq_comap, tangentConeAt_eq_biInter_closure, OpenPartialHomeomorph.tendsto_extend_comp_iff, HasFPowerSeriesAt.eventually_hasSum, ENNReal.tendsto_coe_sub, tendstoIocClassNhds, TopologicalSpace.tendsto_nhds_generateFrom_iff, mem_interior_iff_mem_nhds, Complex.logDeriv_tendsto, nhds_basis_Icc_pos, completeSpace_iff_ultrafilter, ProbabilityTheory.IsCondKernelCDF.tendsto_atTop_one, Metric.closedBall_mem_nhds, nhds_basis_abs_sub_lt, LocallyFinite.exists_forall_eventually_atTop_eventually_eq', eventuallyEq_insert, hasStrictFDerivAt_iff_isLittleOTVS, ENNReal.tendsto_toNNReal_iff', NNReal.tendsto_dist_agmSequences_atTop_zero, exists_seq_strictAnti_tendsto, MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm, isOpenMap_iff_nhds_le, pi_Ico_mem_nhds', nhds_basis_closeds, tendsto_fract_left', tendsto_atBot_ciSup, tendstoIcoClassNhds, tendsto_bdd_div_atTop_nhds_zero, IsTopologicalGroup.mulInvClosureNhd.nhds, disjoint_nhds_cocompact, isLinearTopology_iff_hasBasis_open_twoSidedIdeal, NormedAddCommGroup.summable_imp_tendsto_iff_completeSpace, nhds_cons, tendsto_birkhoffAverage_apply_sub_birkhoffAverage, EReal.nhds_coe, pi_Iic_mem_nhds', map_nhds_induced_of_surjective, IsTopologicalGroup.ext_iff, OpenPartialHomeomorph.isLittleO_congr, MeasureTheory.measurableSet_tendsto_fun, nhds_add_nhds_zero, Filter.tendsto_const_mul_iff, hasBasis_opens_closure, Filter.tendsto_ofReal_iff', Asymptotics.IsEquivalent.tendsto_const, frequently_gt_nhds, Real.tendsto_sigmoid_atTop, hasLineDerivAt_iff_isLittleO_nhds_zero, IsDenseInducing.comap_nhds_neBot, SeparationQuotient.comap_mk_nhds_mk, ptendsto_nhds, ENNReal.tendsto_pow_atTop_nhds_zero_iff, nhds_nhdsAdjoint_of_ne, NNReal.tendsto_atTop_zero_of_summable, t1Space_iff_disjoint_nhds_pure, nhds_basis_Ioo_one_lt, IndiscreteTopology.nhds_eq, Metric.tendsto_nhds_nhds, tendsto_norm_div_self, ContinuousLinearMap.hasBasis_nhds_zero, tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support, WithZeroTopology.nhds_zero_of_units, Seminorm.ball_mem_nhds, eventually_nhds_norm_smul_sub_lt, PointwiseConvergenceCLM.tendsto_nhds, tendsto_nhdsWithin_iff, ENNReal.tendsto_rpow_atTop_of_one_lt_base, eventually_eventuallyEq_nhds, locallyConvexSpace_iff, map_extChartAt_symm_nhdsWithin_range', isSeparatedMap_iff_disjoint_nhds, nhds_false, Submodule.starProjection_tendsto_self, Nat.Partition.tendsto_order_genFun_term_atTop_nhds_top, Polynomial.div_tendsto_zero_iff_degree_lt, Tactic.ComputeAsymptotics.Majorized.tendsto_zero_of_neg, frequently_lt_nhds, tendsto_const_vadd_iff, isClosedMap_iff_comap_nhds_le, mem_nhds_uniformity_iff_right, RestrictedProduct.nhds_zero_eq_map_ofPre, MonotoneOn.tendsto_nhdsLT, ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos, MulOpposite.map_op_nhds, nhdsSet_le, BoxIntegral.HasIntegral.tendsto, SeparationQuotient.tendsto_lift₂_nhds, isProperMap_iff_ultrafilter_of_t2, mem_closure_iff_frequently, isClosed_setOf_tendsto_birkhoffAverage, map_extChartAt_symm_nhdsWithin_range, nhds_one_symm', ENNReal.tendsto_inv_iff, CStarAlgebra.tendsto_mul_left_iff_tendsto_mul_right, Dynamics.ball_dynEntourage_mem_nhds, eventually_nhdsWithin_eventually_nhds_iff_of_isOpen, IsSeqCompact.exists_tendsto_of_frequently_mem, IsUnit.tendsto_const_smul_iff, ENNReal.nhds_top', MeasureTheory.intervalIntegral_tendsto_integral_Iic, tendsto_cfcₙ_fun, isNowhereDense_iff_forall_notMem_nhds, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn, Filter.isInducing_nhds, tendsto_self_mul_const_pow_of_lt_one, frequently_frequently_nhds, MeasureTheory.tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi, chart_source_mem_nhds, hasDerivAt_iff_isLittleO, tendsto_zero_iff_abs_tendsto_zero, MeasureTheory.FinStronglyMeasurable.tendsto_approx, LocallyConvexSpace.convex_basis_zero, ContinuousMap.mem_nhds_iff, uniformity_eq_comap_mul_inv_nhds_one_swapped, Euclidean.ball_mem_nhds, nhds_eq_order, ENNReal.tendsto_nhds_top_iff_nnreal, comap_nhdsWithin_range, T25Space.t2_5, comap_conj_nhds_one, IsTopologicalGroup.tendstoLocallyUniformly_iff, cauchy_map_iff_exists_tendsto, nhdsKer_singleton_eq_ker_nhds, MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos_ne_top, MeasureTheory.tendsto_measure_biInter_gt, intervalIntegral.tendsto_integral_filter_of_dominated_convergence, IsLinearTopology.hasBasis_open_submodule, nhdsWithin_univ, Metric.tendsto_nhds, NormedRing.inverse_one_sub_nth_order, DomMulAct.map_mk_symm_nhds, DomMulAct.comap_mk_nhds, disjoint_nested_nhds_of_not_inseparable, Real.tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici, InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois, GroupFilterBasis.mem_nhds_one, EquicontinuousOn.tendsto_uniformOnFun_iff_pi, Real.tendsto_eulerMascheroniSeq', R0Space.closure_singleton, HasFPowerSeriesOnBall.tendsto_partialSum_prod, WithSeminorms.tendsto_nhds', Complex.tendsto_exp_nhds_zero_iff, ContinuousAt.ne_iff_eventually_ne, MeasureTheory.tendsto_measure_iUnion_atTop, ENNReal.tendsto_atTop_zero_iff_lt_of_antitone, ContinuousLinearMapWOT.le_nhds_iff_forall_dual_apply_le_nhds, comap_norm_nhds_zero, comap_sigmaMk_nhds, IsQuotientCoveringMap.disjoint, WithZeroTopology.tendsto_of_ne_zero, analyticOrderAt_eq_top, Real.comap_exp_nhds_zero, Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain, AnalyticAt.frequently_zero_iff_eventually_zero, HasStrictFDerivAt.eq_implicitFunctionOfComplemented, mem_nhds_iff, ENNReal.hasBasis_nhds_of_ne_top, mem_nhds_prod_iff', lowerSemicontinuous_iff_le_liminf, tendsto_const_nhds, ClusterPt.frequently', HasLineDerivAt.tendsto_slope_zero_right, tendsto_atBot_of_monotone, EReal.tendsto_exp_nhds_zero_nhds_one, LocallyFinite.exists_finset_nhds_support_subset, HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope, Real.Wallis.tendsto_W_nhds_pi_div_two, induced_iff_nhds_eq, UniformOnFun.nhds_eq_of_basis, HasSum.tendsto_sum_nat, pi_Ico_mem_nhds, tendsto_atBot_ciInf, AnalyticAt.exists_eventuallyEq_sum_add_pow_mul, map_add_right_nhds, continuousAt_iff_ultrafilter, FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop, Multipliable.hasProd_iff_tendsto_nat, isOpen_iff_eventually, SeqCompactSpace.tendsto_subseq, tendsto_order_unbounded, Asymptotics.IsLittleO.tendsto_div_nhds_zero, Filter.eventually_nhdsSet_prod_iff, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atBot_zero, tendsto_card_div_pow_atTop_volume, not_tendsto_nhds_of_tendsto_atTop, rtendsto'_nhds, IsLocalMinOn.not_nhds_le_map, ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atTop, Filter.nhds_top, WithZeroTopology.Iio_mem_nhds, isMIntegralCurveAt_eventuallyEq_of_contMDiffAt_boundaryless, EMetric.closedBall_mem_nhds, ENNReal.tendsto_toReal, Filter.mem_nhds_iff, Filter.tendsto_ofReal_iff, EReal.tendsto_coe_atTop, tendsto_zpow_atTop_zero, Asymptotics.isLittleO_pow_pow, nhds_basis_uniformity', HasStrictDerivAt.map_nhds_eq, tendsto_atTop_ciSup, preimage_coe_mem_nhds_subtype, nhds_basis_zero_abs_lt, nhds_eq_iInf_abs_sub, EulerProduct.eulerProduct_completely_multiplicative, Trivialization.tendsto_nhds_iff, WithTop.tendsto_untop, Metric.tendsto_atTop', tendsto_atBot_isLUB, pure_le_nhds, IsOpen.eventually_mem, Real.exp_sub_sum_range_succ_isLittleO_pow, SubmodulesBasis.smul, PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto, HasOuterApproxClosed.tendsto_apprSeq, taylor_tendsto, PeriodPair.compl_lattice_diff_singleton_mem_nhds, EReal.nhds_bot_basis, TopologicalSpace.nhds_mkOfNhds_single, isComplete_iff_ultrafilter, closed_nhds_basis, MeasureTheory.tendsto_integral_approxOn_of_measurable, CPolynomialAt.exists_mem_nhds_cpolynomialOn, UniformSpace.hausdorff.nhds_closure, ProbabilityTheory.Kernel.tendsto_density_atTop_ae_of_antitone, Valued.is_topological_valuation, IsAddFoelner.tendsto_meas_vadd_symmDiff_vadd, Bornology.isVonNBounded_iff_absorbing_le, DomMulAct.map_mk_nhds, one_le_nhds_iff, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp, NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT, mem_nhds_uniformity_iff_left, nhds_true, DenseRange.exists_seq_strictMono_tendsto, mem_nhds_left, Real.comap_exp_nhds_exp, tendsto_norm_sub_self, MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto, Real.tendsto_exp_neg_atTop_nhds_zero, eventuallyEq_toIcoDiv_nhds, tendsto_smoothingFun_comp, tendsto_nhds_Prop, PartitionOfUnity.exists_finset_nhds, MeasureTheory.FiniteMeasure.tendsto_measure_iUnion_accumulate, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_antitone, MeasureTheory.tendsto_measure_of_tendsto_indicator, Hyperreal.tendsto_iff_forall, t0Space_iff_nhds_injective, CofiniteTopology.mem_nhds_iff, MeasureTheory.SimpleFunc.tendsto_eapprox, le_nhds_iff, IsTopologicalGroup.isOpenMap_iff_nhds_one, MeasureTheory.tendstoInMeasure_iff_norm, OnePoint.comap_coe_nhds, IsAdic.hasBasis_nhds, AbsolutelyContinuousOnInterval.tendsto_volume_totalLengthFilter_nhds_zero, ENNReal.tendsto_cofinite_zero_of_tsum_ne_top, PadicInt.fwdDiff_tendsto_zero, SuccOrder.nhdsLE_eq_nhds, LocallyFinite.exists_forall_eventually_eq_prod, IsSeqCompact.exists_tendsto, principal_nhdsKer_singleton, Metric.disjoint_nhds_cobounded, EReal.nhds_top', MeasureTheory.Integrable.tendsto_eLpNorm_condExp, AntitoneOn.tendsto_nhdsWithin_Ioo_right, HasStrictFDerivAt.approximates_deriv_on_nhds, Filter.HasBasis.equicontinuousAt_iff_right, contDiffAt_one_iff, Equicontinuous.tendsto_uniformFun_iff_pi, ZLattice.covolume.tendsto_card_div_pow, prod_mem_nhds_iff, hasGradientAt_iff_isLittleO, ClusterPt.neBot, IsLinearTopology.hasBasis_submodule, PartitionOfUnity.eventually_fintsupport_subset, IsFoelner.tendsto_meas_smul_symmDiff, IsTopologicalAddGroup.ext_iff, hasDerivAtFilter_iff_tendsto_slope, fderivWithin_eventually_congr_set', extChartAt_target_union_compl_range_mem_nhds_of_mem, Ctop.Realizer.nhds_σ, nhds_smul₀, HasFDerivAt.isBigOTVS_sub, MeasureTheory.StronglyMeasurable.measurableSet_exists_tendsto, IsTopologicalGroup.exists_antitone_basis_nhds_one, VitaliFamily.ae_tendsto_lintegral_div, ProbabilityTheory.tendsto_integral_truncation, VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet, nhdsWithin_eq_map_subtype_coe, clusterPt_iff_frequently', Metric.exists_forall_closedEBall_subset_aux₁, ModuleFilterBasis.smul_right, LocallyFinite.exists_forall_eventually_atTop_eventuallyEq, Metric.closedBall_mem_nhds_of_mem, OnePoint.tendsto_nhds_infty, nhds_top_basis_Ici, WeaklyLocallyCompactSpace.exists_compact_mem_nhds, Real.GammaSeq_tendsto_Gamma, Multipliable.tendsto_cofinite_one, mapClusterPt_iff_ultrafilter, FloorSemiring.tendsto_pow_div_factorial_atTop, tendsto_one_div_add_atTop_nhds_zero_nat, TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq, ENat.mem_nhds_iff, AbsConvexOpenSets.coe_nhds, MeasureTheory.tendstoInMeasure_iff_measureReal_dist, MeasureTheory.FiniteMeasure.tendsto_iff_forall_lintegral_tendsto, Complex.comap_exp_nhds_zero, OpenPartialHomeomorph.eventually_left_inverse, Summable.tendsto_alternating_series_tsum, ProbabilityTheory.strong_law_ae, ENNReal.tendsto_tsum_compl_atTop_zero, nhds_basis_Icc_one_lt, isCompact_isClosed_basis_nhds, TendstoUniformlyOnFilter.tendsto_at, Real.tendsto_of_bddAbove_monotone, MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto, isOpen_setOf_disjoint_nhds_nhds, IsTopologicalAddGroup.exists_antitone_basis_nhds_zero, exists_fun_of_mem_tangentConeAt, SmoothBumpFunction.support_mem_nhds, PredOrder.nhdsGE_eq_nhds, Monotone.tendsto_nhdsLT, cauchy_iff_exists_le_nhds, cauchySeq_tendsto_of_complete, TopologicalSpace.IsTopologicalBasis.mem_nhds, eventually_nnnorm_sub_lt, MeasureTheory.AECover.integral_tendsto_of_countably_generated, ProbabilityTheory.Kernel.trajContent_tendsto_zero, has_fderiv_at_filter_real_equiv, Homeomorph.map_nhds_eq, mem_closure_iff_comap_neBot, locPathConnectedSpace_iff_pathComponentIn_mem_nhds, compl_singleton_mem_nhds_iff, Metric.eventually_nhds_iff, RingSubgroupsBasis.hasBasis_nhds_zero, tendsto_integral_exp_smul_cocompact, BoxIntegral.Integrable.to_subbox_aux, map_fst_nhdsWithin, EulerProduct.eulerProduct, StronglyLocallyContractibleSpace.contractible_basis, hasDerivAt_iff_tendsto_slope_left_right, UniformOnFun.tendsto_iff_tendstoUniformlyOn, Asymptotics.isBigOTVS_iff_smallSets, contractible_subset_basis, locallyConnectedSpace_iff_connected_subsets, MeasureTheory.Integrable.tendsto_ae_condExp, ProbabilityTheory.IsMeasurableRatCDF.tendsto_atBot_zero, Homeomorph.isBigOWith_congr, eventually_riemmanianEDist_lt, InnerProductSpace.HarmonicAt.eventually, tendsto_prod_filter_iff, MeasureTheory.tendsto_of_forall_isClosed_limsup_le, disjoint_nhds_nhds_iff_not_specializes, Real.tendsto_exp_comp_nhds_zero, EMetric.tendsto_nhds, IsLinearTopology.hasBasis_twoSidedIdeal, WithAbs.tendsto_one_div_one_add_pow_nhds_one, nhds_order_unbounded, Valued.tendsto_zero_pow_of_le_exp_neg_one, tendsto_norm_div_self_nhdsGE, Dense.exists_seq_strictAnti_tendsto_of_lt, hasStrictFDerivAt_iff_isLittleO, CPolynomialAt.eventually_cpolynomialAt, Inseparable.nhds_eq, tendsto_sub_mul_tsum_nat_cpow, IsSeqCompact.subseq_of_frequently_in, intervalIntegral.FTCFilter.le_nhds, Besicovitch.ae_tendsto_rnDeriv, UniformFun.hasBasis_nhds_zero, EReal.mem_nhds_bot_iff, Filter.tendsto_add_const_iff, MvPowerSeries.LinearTopology.isTopologicallyNilpotent_iff_constantCoeff, NNReal.tendsto_agmSequences_snd_agm, LocallyFinite.exists_finset_support, Ctop.Realizer.nhds_F, map_nhds, ContinuousAlgEquiv.symm_map_nhds_eq, Filter.tendsto_inv₀_cobounded, DenseRange.exists_seq_strictMono_tendsto_of_lt, Euclidean.nhds_basis_closedBall, eventually_abs_sub_lt, IsCompact.tendsto_subseq', Metric.tendsto_nhdsWithin_nhds, inseparable_def, QuotientGroup.nhds_one_hasBasis, Valued.tendsto_zero_pow_of_v_lt_one, Polynomial.div_tendsto_atBot_zero_of_degree_lt, nhds_zero_symm, PartitionOfUnity.exists_finset_nhds_support_subset, not_tendsto_nhds_of_tendsto_atBot, eventually_lt_nhds, t2_separation_nhds, le_nhds_of_cauchy_adhp, LightProfinite.continuous_iff_convergent, LinearIndependent.eventually, nhds_pi, tendsto_order, MeasureTheory.tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure, Real.tendsto_integral_gaussian_smul', nhds_basis_Ioo_one_lt_of_one_lt, tendsto_fract_right', hasGradientAt_iff_isLittleO_nhds_zero, nhds_inter_eq_singleton_of_mem_discrete, EisensteinSeries.tendsto_zero_inv_linear_sub, SuccOrder.nhds_eq_pure, tendsto_riemannZeta_sub_one_div, HasStrictFDerivAt.map_nhds_eq_of_surj, ZetaAsymptotics.tendsto_Gamma_term_aux, Summable.tendsto_atTop_zero, Filter.HasBasis.nhds, MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto, MulOpposite.comap_unop_nhds, SummationFilter.hasSum_symmetricIoc_int_iff, nhds_injective, MeasureTheory.tendstoInMeasure_iff_dist, CofiniteTopology.nhds_eq, nhdsWithin_eq_iff_eventuallyEq, Antitone.tendsto_nhdsGT, isLocalHomeomorph_iff_isOpenEmbedding_restrict, SeminormedAddGroup.disjoint_nhds_zero, IsGLB.exists_seq_strictAnti_tendsto_of_notMem, UniformFun.tendsto_iff_tendstoUniformly, MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt, IsLocallyConstant.iff_eventually_eq, ContinuousAt.stronglyMeasurableAtFilter, Trivialization.coe_fst_eventuallyEq_proj', LowerSemicontinuousAt.le_liminf, Asymptotics.isLittleO_pow_id, MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset, VectorField.lieBracketWithin_eventually_congr_set', Complex.tendsto_one_add_div_pow_exp, MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_tendsto, ENNReal.tendsto_atTop_zero_of_tsum_ne_top, ENNReal.tendsto_coe_toNNReal, ENat.nhds_eq_pure, spectrum.gelfand_formula, tendsto_pow_atTop_nhds_zero_iff_norm_lt_one, Rat.cocompact_inf_nhds_neBot, r1Space_iff_inseparable_or_disjoint_nhds, IsRightUniformAddGroup.uniformity_eq, MeasureTheory.tendsto_of_uncrossing_lt_top, tendsto_measure_cthickening, Filter.tendsto_nhds_atBot, nhdsWithin_eq_nhds, Filter.tendsto_nhds, UniformContinuous₂.tendstoUniformly, VitaliFamily.ae_tendsto_limRatio, Asymptotics.superpolynomialDecay_iff_zpow_tendsto_zero, MeasureTheory.Measure.div_mem_nhds_one_of_haar_pos, Filter.nhds_inf, HasLineDerivAt.tendsto_slope_zero, Complex.tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero, Real.exists_seq_rat_strictAnti_tendsto, EisensteinSeries.tendsto_e2Summand_atTop_nhds_zero, Real.tendsto_sin_neg_pi_div_two, tendsto_measure_Icc, tendsto_logDeriv_euler_sin_div, tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded, tendsto_star, Real.tendsto_exp_nhds_zero_nhds_one, List.Vector.tendsto_cons, Topology.IsOpenEmbedding.image_mem_nhds, ENNReal.tendsto_atTop, mem_nhdsWithin_iff_eventuallyEq, tendsto_mul_coprod_nhds_zero_inf_of_disjoint_cocompact, SummationFilter.hasSum_symmetricIcc_iff, DifferentiableAt.isBigOTVS_sub, CompactExhaustion.exists_mem_nhds, nhds_basis_balanced, IsContDiffImplicitAt.apply_implicitFunction, HasStrictFDerivAt.isLittleO, Valued.hasBasis_nhds_zero, HasStrictFDerivAt.exists_lipschitzOnWith, isCobounded_ge_nhds, IsBoundedLinearMap.lim_zero_bounded_linear_map, eventually_norm_sub_lt, MeasureTheory.tendsto_diracProba_iff_tendsto, frequently_nhds_subtype_iff, Irrational.eventually_forall_le_dist_cast_div_of_denom_le, Topology.IsUpper.tendsto_nhds_iff_not_le, MonotoneOn.tendsto_nhdsGT, HasStrictFDerivAt.map_implicitFunction_eq, MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos, MeasureTheory.Measure.mem_support_iff, IsLinearTopology.hasBasis_open_ideal, WithZeroTopology.hasBasis_nhds_of_ne_zero, MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre, comap_mabs_nhds_one, Real.isEquivalent_sin, tendsto_rpow_atTop_of_base_gt_one, Real.tendsto_sigmoid_atBot, IsDiscrete.exists_nhds_eq_one_of_image_mulRight_inter_nonempty, Real.tendsto_harmonic_sub_log, Complex.isBigO_re_sub_re, Filter.nhds_bot, mem_nhds_subtype, contMDiffAt_iff_contMDiffOn_nhds, ContinuousMultilinearMap.hasBasis_nhds_zero, OpenPartialHomeomorph.isBigO_congr, tendsto_indicator_const_iff_forall_eventually, IsValuativeTopology.mem_nhds_iff', ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one, le_nhds_add, eventually_ne_nhds, CircleDeg1Lift.tendsto_translation_number', ENNReal.tendsto_rpow_at_top, nhds_nhdsAdjoint, nhds_prod_le_of_disjoint_cocompact, TendstoUniformly.tendsto_at, pcontinuous_iff', Compactum.le_nhds_of_str_eq, tendsto_atBot_of_eventually_const, Filter.tendsto_const_add_iff, IsLindelof.disjoint_nhdsSet_left, isMIntegralCurveAt_iff, ProperlyDiscontinuousVAdd.exists_nhds_image_vadd_eq_self, tendsto_nat_floor_mul_div_atTop, le_nhdsAdjoint_iff', controlled_sum_of_mem_closure_range, map_extChartAt_nhds_of_boundaryless, HasStrictFDerivAt.eventually_left_inverse, ENNReal.tendsto_pow_atTop_nhds_top_iff, Trivialization.coe_fst_eventuallyEq_proj, iSup_nhds_le_uniformity, BoundedLENhdsClass.isBounded_le_nhds, nhdsKer_singleton_subset_iff_mem_nhds, HurwitzZeta.completedHurwitzZetaEven_residue_one, uniformity_eq_comap_inv_mul_nhds_one, MeasureTheory.tendsto_indicator_ge, ker_nhds_eq_specializes, Summable.hasSum_iff_tendsto_nat, MeasureTheory.Measure.notMem_support_iff, lift'_nhds_closure, EReal.tendsto_coe_ennreal, Metric.eventually_nhds_zero_forall_closedEBall_subset, Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhds, exists_seq_strictAnti_strictMono_tendsto, nhds_eq_nhdsWithin_sup_nhdsWithin, OpenPartialHomeomorph.eventually_right_inverse, Isometry.tendsto_nhds_iff, nhds_neg, tendsto_natCast_div_add_atTop, MeasureTheory.ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds, VitaliFamily.ae_tendsto_average_norm_sub, HasLineDerivAt.tendsto_slope_zero_left, tendsto_nhds_iff_meromorphicOrderAt_nonneg, AddOpposite.comap_unop_nhds, UpperHemicontinuousAt.forall_isOpen, tendstoUniformlyOn_singleton_iff_tendsto, MeasureTheory.tendsto_setIntegral_of_antitone, EMetric.nhds_basis_eball, MeasureTheory.tendsto_measure_vadd_diff_isCompact_isClosed, nhds_translation_mul_inv₀, MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset, AddGroupFilterBasis.nhds_eq, NNReal.tendsto_of_antitone, TendstoUniformlyOn.tendsto_at, OpenSubgroup.mem_nhds_one, tendsto_pow_div_pow_atTop_zero, tendsto_nhdsWithin_range, Continuous.nhds, ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ, nhds_basis_Ioo_pos, Prod.tendsto_iff, ENNReal.hasBasis_nhds_of_ne_top', MeasureTheory.tendsto_measure_Iic_atTop, Real.zero_at_infty_fourierIntegral, Bornology.IsVonNBounded.tendsto_smallSets_nhds, ProbabilityTheory.Kernel.tendsto_integral_density_of_monotone, natCast_le_analyticOrderAt, map_snd_nhdsWithin, ENNReal.tendsto_toNNReal, AnalyticAt.eventually_constant_or_nhds_le_map_nhds, Complex.tendsto_self_mul_Gamma_nhds_zero, ImplicitFunctionData.map_nhds_eq, IsOpenMap.nhds_le, set_smul_mem_nhds_zero_iff, TopologicalSpace.nhds_generateFrom, IsLocallyConstant.eventually_eq, IsTopologicalAddGroup.addNegClosureNhd.nhds, IsCompact.disjoint_nhdsSet_left, tendsto_rpow_div_mul_add, MeasureTheory.tendsto_measure_of_tendsto_indicator_of_isFiniteMeasure, OnePoint.nhds_coe_eq, tendsto_rpow_atTop_of_base_lt_one, ZeroAtInftyContinuousMap.zero_at_infty', eventually_eventuallyLE_nhds, spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius, IsClosedMap.comap_nhds_le, MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto_aux, HasDerivAt.tendsto_slope_zero_left, nhds_add, RCLike.tendsto_add_mul_div_add_mul_atTop_nhds, nhds_inl, ProbabilityTheory.Kernel.tendsto_densityProcess_atTop_empty_of_antitone, IsLocalExtrOn.not_nhds_le_map, frequently_nhds_iff, nhds_toAdd, ProbabilityTheory.IsRatCondKernelCDF.tendsto_atTop_one, Complex.tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero, Multipliable.tendsto_atTop_one, finprod_eventually_eq_prod, Filter.Germ.value_smul, IsUnit.smul_mem_nhds_smul_iff, tendsto_arithGeom_nhds_of_lt_one, upperHemicontinuousAt_iff_preimage_Iic, nhds_zero_add_nhds, IsLindelof.disjoint_nhdsSet_right, mfderivWithin_eventually_congr_set', eventually_homothety_mem_of_mem_interior, Complex.isEquivalent_sinh, exists_nhds_disjoint_closure, isBounded_ge_nhds, HasProd.tendsto_prod_nat, ENNReal.coe_range_mem_nhds, LocallyFinite.exists_finset_mulSupport, tendsto_iff_tendsto_subseq_of_monotone, Filter.nhds_eq, ContinuousLinearMapWOT.hasBasis_seminorms, ENNReal.tendsto_atTop_zero_iff_le_of_antitone, contDiffPointwiseHolderAt_iff, eventually_nhdsWithin_sign_eq_of_deriv_neg, Asymptotics.isLittleO_pow_sub_pow_sub, DomAddAct.comap_mk.symm_nhds, MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre_nat, TendstoUniformlyOn.tendsto_comp, ProperlyDiscontinuousSMul.exists_nhds_image_smul_eq_self, HasFPowerSeriesAt.isBigO_image_sub_norm_mul_norm_sub, isBigO_riemannZeta_sub_one_div, pathConnected_subset_basis, MeasureTheory.UnifIntegrable.unifIntegrable_of_ae_tendsto, exists_seq_tendsto_sSup, HasFPowerSeriesAt.eventually_eq_zero, Filter.tendsto_sub_const_iff, Asymptotics.isLittleO_id_one, MeasureTheory.tendsto_measure_iInter_le, tendsto_measure_thickening, List.tendsto_insertIdx', compactSpace_uniformity, tendsto_rpow_sub_one_log, AffineSpace.nhds_bind_asymptoticNhds, ENNReal.tendsto_mul, Cauchy.le_nhds_lim, SmoothBumpFunction.tsupport_mem_nhds, toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhds, hasFDerivAt_iff_tendsto, pi_Ioc_mem_nhds, MeasureTheory.tendsto_measure_norm_gt_of_isTightMeasureSet, tendsto_nat_floor_div_atTop, ENNReal.nhds_coe, IsTopologicalAddGroup.isOpenMap_iff_nhds_zero, nhds_inr, SuccOrder.hasBasis_nhds_Ioc_of_exists_lt, MeasureTheory.ProbabilityMeasure.tendsto_measure_iUnion_accumulate, NNRat.tendsto_inv_atTop_nhds_zero_nat, tendsto_zero_of_meromorphicOrderAt_pos, MeasureTheory.intervalIntegral_tendsto_integral, tendsto_pow_const_mul_const_pow_of_abs_lt_one, Bornology.isVonNBounded_iff_smul_tendsto_zero, MeasureTheory.Submartingale.ae_tendsto_limitProcess_of_uniformIntegrable, EReal.tendsto_const_div_atTop_nhds_zero_nat, ContinuousLinearEquiv.nhds, tendsto_inv_atBot_zero, nhdsLT_sup_nhdsGE, nhds_bind_nhds, Complex.log_sub_self_isBigO, IsAdic.hasBasis_nhds_zero, OpenPartialHomeomorph.map_extend_nhds, ModelWithCorners.symm_map_nhdsWithin_range, ENNReal.tendsto_nat_nhds_top, PartitionOfUnity.eventually_finsupport_subset, WithSeminorms.tendsto_nhds, IsCompact.ultrafilter_le_nhds', EMetric.tendsto_nhds_nhds, tendsto_integral_mul_one_add_inv_smul_sq_pow, Asymptotics.isLittleO_iff_tendsto', Complex.arg_eq_nhds_of_im_neg, Uniform.tendsto_congr, expNegInvGlue.tendsto_polynomial_inv_mul_zero, tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact, Complex.tendsto_exp_comap_re_atBot, intervalIntegral.FTCFilter.nhdsUniv, Homeomorph.comap_nhds_eq, Filter.IsApproximateUnit.nhds_one, nhds_top, pi_Ici_mem_nhds', IsValuativeTopology.mem_nhds_zero_iff, AddSubmonoid.mem_nhds_zero, Asymptotics.isLittleOTVS_iff_smallSets, tendsto_atTop_isGLB, nhds_hasBasis_absConvex, nhds_basis_Ioo_pos_of_pos, Ne.nhdsWithin_compl_singleton, smul_mem_nhds_self, Metric.continuous_iff', Asymptotics.continuousAt_iff_isLittleO, mem_nhdsWithin_iff_eventually, MeasureTheory.intervalIntegral_tendsto_integral_Ioi, Asymptotics.isLittleOTVS_iff_tendsto_div, AddChar.tendsto_eval_one_sub_pow, Complex.tendsto_euler_sin_prod, ContinuousMap.nhds_compactOpen_eq_iInf_nhds_induced, MeasureTheory.tendsto_zero_of_hasDerivAt_of_integrableOn_Iic, ProbabilityTheory.Kernel.tendsto_integral_density_of_antitone, ContinuousWithinAt.nhds, TopologicalSpace.IsTopologicalBasis.nhds_basis_closure, Continuous.limUnder_eq, disjoint_nhds_atBot_iff, uniformity_eq_comap_mul_inv_nhds_one, OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq_aux, HurwitzZeta.hurwitzZeta_residue_one, mem_nhdsSet_iff_forall, Antitone.tendsto_leftLim, nhds_comap_dist, PredOrder.hasBasis_nhds_Ioc_of_exists_gt, HasFiniteFPowerSeriesAt.eventually_zero_of_bound_zero, MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae, tendsto_pi_nhds, UniformSpace.mem_nhds_iff_symm, tendsto_iff_tendsto_subseq_of_antitone, WithZeroTopology.hasBasis_nhds_zero, Filter.Germ.sliceRight_coe, uniformity_eq_comap_nhds_zero, pi_Ioi_mem_nhds', tendsto_measure_Icc_nhdsWithin_right, NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat, PowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, TopologicalSpace.nhds_mkOfNhds_of_hasBasis, nhds_nhds_eq_uniformity_uniformity_prod, NumberField.Ideal.tendsto_norm_le_div_atTop₀, AnalyticAt.analyticOrderAt_eq_natCast, MeasureTheory.IsLocallyFiniteMeasure.finiteAtNhds, ProbabilityTheory.strong_law_aux6, Topology.IsLower.tendsto_nhds_iff_lt, nhds_nil, clusterPt_iff_not_disjoint, compl_singleton_mem_nhds, Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain', IsLeftUniformAddGroup.uniformity_eq, isLocalHomeomorphOn_iff_isOpenEmbedding_restrict, MeasureTheory.tendsto_measure_Ioc_atBot, nhds_def, tendsto_integral_mulExpNegMulSq_comp, compact_open_separated_mul_left, UniformSpace.nhds_eq_comap_uniformity, ZeroAtInftyContinuousMapClass.zero_at_infty, RestrictedProduct.nhds_eq_map_structureMap, tendsto_of_liminf_eq_limsup, RingSubgroupsBasis.hasBasis_nhds, LinearGrowth.tendsto_atTop_of_linearGrowthInf_pos, NormedRing.inverse_add, Subadditive.tendsto_lim, ENNReal.nhds_top_basis, LinearMap.hasBasis_weakBilin, Real.tendsto_mul_log_one_add_div_atTop, nhds_swap, Topology.IsInducing.tendsto_nhds_iff, QuotientAddGroup.nhds_zero_hasBasis, controlled_prod_of_mem_closure_range, ZLattice.covolume.tendsto_card_le_div', MeasureTheory.SimpleFunc.tendsto_approxOn, eventually_mem_nhds_iff, AddGroupFilterBasis.nhds_zero_eq, EReal.tendsto_exp_nhds_top_nhds_top, isLinearTopology_iff_hasBasis_ideal, continuousOn_update_iff, nhds_le_uniformity, Filter.top_smul_nhds_zero, BoundedContinuousFunction.tendsto_integral_of_forall_integral_le_liminf_integral, tendsto_ne_zero_of_meromorphicOrderAt_eq_zero, Summable.tendsto_sum_tsum_nat, eventually_gt_nhds, eventually_nhdsWithin_sign_eq_of_deriv_pos, AnalyticAt.analyticOrderNatAt_eq_iff, nhds_eq_iInf_mabs_div, isFoelner_iff, IsUniformAddGroup.cauchy_iff_tendsto_swapped, Ctop.Realizer.mem_nhds, ENNReal.nhds_of_ne_top, NNReal.tendsto_sum_nat_add, ContractingWith.tendsto_iterate_efixedPoint, HasStrictDerivAt.eventually_right_inverse, nhds_eq_nhds_emetric_ball, ContinuousMap.tendsto_iff_tendstoUniformly, TopologicalSpace.OpenNhdsOf.basis_nhds, nhds_translation_mul_inv, Ideal.hasBasis_nhds_zero_adic, finsum_eventually_eq_sum, SmoothBumpCovering.eventuallyEq_one, NormedRing.inverse_add_norm, List.tendsto_cons_iff, nhds_subtype_eq_comap, IsFoelner.tendsto_meas_smul_symmDiff_smul, tendsto_integral_exp_smul_cocompact_of_inner_product, contMDiffAt_iff_contMDiffAt_nhds, PredOrder.nhds_eq_pure, HurwitzZeta.completedCosZeta_residue_zero, ContDiffAt.restrictScalars_iteratedFDeriv_eventuallyEq, uniformity_eq_comap_nhds_zero_left, tendsto_of_antitone, properSMul_iff_continuousSMul_ultrafilter_tendsto_t2, tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero, AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero, nhds_inv₀, UpperHalfPlane.qParam_tendsto_atImInfty, WithZeroTopology.nhds_coe_units, EMetric.exists_forall_closedBall_subset_aux₁, DifferentiableAt.isBigO_sub, ModelWithCorners.map_nhds_eq, notMem_tsupport_iff_eventuallyEq, upperHemicontinuous_iff_preimage_Iic, MeasureTheory.tendsto_of_forall_isClosed_limsup_le_nat, Uniform.continuousAt_iff'_left, Filter.tendsto_div_const_iff, AddOpposite.comap_op_nhds, MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm', UniformSpace.nhds_basis_clopens, extChartAt_target_eventuallyEq', tendsto_smoothingFun_of_map_one_le_one, extChartAt_source_mem_nhds, smul_mem_nhds_smul_iff₀, LowerSemicontinuous.le_liminf, NormedAddCommGroup.tendsto_nhds_nhds, VitaliFamily.ae_tendsto_div, WithZeroTopology.nhds_of_ne_zero, AddGroupFilterBasis.nhds_zero_hasBasis, VitaliFamily.ae_tendsto_measure_inter_div, isCompact_iff_ultrafilter_le_nhds, hasDerivAt_iff_tendsto_slope_zero, OpenAddSubgroup.mem_nhds_zero, nhds_inf, tendsto_self_mul_const_pow_of_abs_lt_one, LocallyFinite.iInter_compl_mem_nhds, IsClosed.compl_mem_nhds, ContinuousAt.eventually_lt, zero_cpow_eq_nhds, SeminormFamily.basisSets_mem_nhds, Metric.continuousAt_iff', Antitone.tendsto_setIntegral, extChartAt_source_mem_nhds', ArithmeticFunction.IsMultiplicative.eulerProduct, ContinuousAlternatingMap.hasBasis_nhds_zero, lowerHemicontinuousAt_iff, AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux, CauchySeq.tendsto_limUnder, interior_setOf_eq, HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp, tendsto_fib_div_fib_succ_atTop, MvPowerSeries.hasEval_def, NormedRing.inverse_add_norm_diff_second_order, ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atBot, ContractingWith.exists_fixedPoint, MeasureTheory.tendsto_ae_condExp, BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq, IsCompact.prod_nhdsSet_eq_biSup, eventually_norm_symmL_trivializationAt_self_comp_lt, WithTop.tendsto_untopA, IsOpenQuotientMap.map_nhds_eq, Asymptotics.isLittleO_norm_pow_norm_pow, Submonoid.mem_nhds_one, tendstoIccClassNhds, ProbabilityTheory.Kernel.tendsto_densityProcess_fst_atTop_univ_of_monotone, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_zero_of_antitone, IsLeftUniformGroup.uniformity_eq, tendsto_prod_top_iff, CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers, EMetric.tendstoLocallyUniformly_iff, tendsto_lift'_closure_nhds, IsValuativeTopology.hasBasis_nhds_zero', t2Space_iff_disjoint_nhds, MeasureTheory.tendsto_of_forall_isClosed_limsup_real_le', UniformSpace.hasBasis_nhds, EMetric.tendsto_atTop, List.tendsto_eraseIdx, HasStrictFDerivAt.localInverse_tendsto, Real.taylor_tendsto, BoundedGENhdsClass.isBounded_ge_nhds, tendsto_uniformity_iff_dist_tendsto_zero, Specializes.nhds_le_nhds, Filter.Tendsto.nhds_atBot, IsOpenMap.map_nhds_eq, GroupFilterBasis.nhds_one_hasBasis, Polynomial.div_tendsto_leadingCoeff_div_of_degree_eq, List.tendsto_sum, vadd_mem_nhds_self, tendsto_log_div_rpow_nhdsGT_zero, Ioo_mem_nhds, Filter.mem_nhds_iff', SeminormFamily.basisSets_smul, inf_nhds_atTop, UpperSemicontinuousAt.limsup_le, forall_restrictGermPredicate_iff, nhdsSet_Iic, Ultrafilter.le_nhds_lim, hasGradientAt_iff_tendsto, tendsto_floor_left', VitaliFamily.ae_eventually_measure_zero_of_singular, Besicovitch.ae_tendsto_measure_inter_div, RegularSpace.regular, IsOpen.mem_nhds_iff, Homeomorph.isBigO_congr, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto, UniformSpace.Core.nhds_toTopologicalSpace, Set.pairwiseDisjoint_nhds, Seminorm.continuous_iff, SchwartzMap.tendsto_cocompact, tendsto_sub_comap_self, IsGLB.frequently_nhds_mem, Continuous.tendsto, ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn, ProperlyDiscontinuousSMul.exists_nhds_disjoint_image, PadicInt.continuousAddCharEquiv_of_norm_mul_symm_apply, IsRightUniformGroup.uniformity_eq, upperSemicontinuousAt_iff_limsup_le, MonotoneOn.tendsto_nhdsWithin_Ioo_right, Ico_mem_nhds_iff, nhds_basis_opens', contDiffAt_succ_iff_hasFDerivAt, tendsto_conj_nhds_one, ge_mem_nhds, ENNReal.tendsto_toNNReal_iff, mem_closure_iff_seq_limit, HasFPowerSeriesWithinOnBall.tendsto_partialSum_prod, ProbabilityTheory.IsRatCondKernelCDF.tendsto_atBot_zero, ContractingWith.tendsto_iterate_fixedPoint, eventually_nhds_iff, SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq, IsValuativeTopology.hasBasis_nhds, HasFDerivAt.lim, CauSeq.tendsto_limit, Polynomial.tendsto_nhds_iff, map_extChartAt_nhds', isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image, compact_basis_nhds, Real.tendsto_exp_atBot, Metric.ball_mem_nhds, MonotoneOn.tendsto_nhdsWithin_Ioo_left, eventuallyEq_nhdsWithin_iff, VitaliFamily.ae_tendsto_lintegral_div', SummationFilter.hasProd_symmetricIco_int_iff, HasStrictFDerivAt.isEquivalent_sub, SmoothPartitionOfUnity.eventually_fintsupport_subset, TrivSqZeroExt.nhds_inl, IsUniformGroup.cauchy_map_iff_tendsto, SummationFilter.hasSum_symmetricIco_int_iff, ContDiffAt.laplacian_add_nhds, OpenPartialHomeomorph.extend_target_eventuallyEq, Filter.nhds_principal, EReal.tendsto_coe, tendsto_iff_forall_eval_tendsto_topDualPairing, tendsto_pow_neg_atTop, nhds_top_order, tendsto_add_mul_div_add_mul_atTop_nhds, Complex.isBigO_im_sub_im, Homeomorph.nhds_eq_comap, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess, codiscreteWithin_iff_locallyFiniteComplementWithin, tendsto_one_div_atTop_nhds_zero_nat, tendsto_nhds_iff_seq_tendsto, tendsto_pow_atTop_nhds_zero_of_abs_lt_one, IsLinearTopology.hasBasis_submodule', Filter.nhds_pure, isOpen_setOf_eventually_nhds, IsLocalDiffeomorphAt.localInverse_eventuallyEq_left, Uniform.tendsto_nhds_right, tendsto_atTop_of_eventually_const, NNReal.hasSum_iff_tendsto_nat, EReal.tendsto_exp_nhds_bot_nhds_zero, Metric.eball_mem_nhds, ENNReal.tendsto_coe, nonneg_nhds_iff, TopologicalSpace.FirstCountableTopology.tendsto_subseq, eventually_norm_symmL_trivializationAt_comp_self_lt, MeasureTheory.tendsto_measure_sigmaFiniteSetGE, CompactConvergenceCLM.hasBasis_nhds_zero, DomMulAct.comap_mk.symm_nhds, OnePoint.comap_coe_nhds_infty, IsValuativeTopology.hasBasis_nhds_zero, SmoothBumpFunction.eventuallyEq_of_mem_source, MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm, eventually_nhdsNE_eventually_nhds_iff, cauchySeq_iff_le_tendsto_0, ENNReal.tendsto_ofReal_atTop, nhdsSet_Ici, EMetric.cauchySeq_iff_le_tendsto_0, MeasureTheory.Measure.notMem_support_iff_exists, dslope_eventuallyEq_slope_of_ne, Complex.tendsto_one_add_div_cpow_exp, tendsto_norm_one, tendsto_pure_nhds, HasFPowerSeriesOnBall.tendsto_partialSum, tendsto_iff_norm_div_tendsto_zero, upperSemicontinuous_iff_limsup_le, TendstoLocallyUniformlyOn.tendsto_at, R1Space.specializes_or_disjoint_nhds, MeasureTheory.eventually_nhds_zero_measure_vadd_diff_lt, nhds_subtype, PrimeSpectrum.nhdsOrderEmbedding_apply, IsContDiffImplicitAt.eventually_implicitFunction_apply_eq, Euclidean.nhds_basis_ball, HasOuterApproxClosed.tendsto_lintegral_apprSeq, TopologicalGroup.isOpenMap_iff_nhds_one, Filter.HasBasis.nhds', MeasureTheory.tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum, HasFDerivAt.lim_real, Real.tendsto_log_comp_add_sub_log, Complex.exp_sub_sum_range_succ_isLittleO_pow, ENNReal.nhds_zero_basis, HasCompactMulSupport.is_one_at_infty, BoxIntegral.Box.exists_seq_mono_tendsto, disjoint_nhds_nhds_iff_not_inseparable, IsAddQuotientCoveringMap.disjoint, eventually_enorm_mfderiv_extChartAt_lt, tendsto_nhdsWithin_iff_subtype, HasFPowerSeriesOnBall.eventually_hasSum, mem_nhds_induced, nhds_translation_add_neg, disjoint_nhds_nhdsSet, ENNReal.tendsto_inv_nat_nhds_zero, MeasureTheory.tendstoInMeasure_iff_measureReal_enorm, tendsto_const_smul_iff, List.tendsto_prod, t2_separation_compact_nhds, smul_mem_nhds_smul_iff, union_mem_nhds_of_mem_nhdsWithin, nhdsWithin_le_nhds, le_nhds_of_cauchy_adhp_aux, continuousAt_iff_punctured_nhds, cauchySeq_tendsto_of_isComplete, ProbabilityTheory.IsCondKernelCDF.tendsto_atBot_zero, Topology.IsEmbedding.tendsto_nhds_iff, ZLattice.covolume.tendsto_card_div_pow', Topology.isInducing_iff_nhds, MeasureTheory.tendsto_eLpNorm_condExp, Filter.Eventually.eventually_nhdsSet, nhds_le_of_le, comap_norm_nhds_one, EisensteinSeries.tendsto_zero_inv_linear, pi_Iio_mem_nhds', hasDerivAtFilter_iff_tendsto, MvPowerSeries.coeff_zero_iff, interior_eq_nhds, unitInterval.tendsto_sigmoid_atTop, Topology.IsLower.tendsto_nhds_iff_not_le, HasFPowerSeriesAt.eventually_differentiableAt, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos, supportDiscreteWithin_iff_locallyFiniteWithin, Ioc_mem_nhds_iff, EReal.tendsto_coe_nhds_bot_iff, tendsto_const_mul_pow_nhds_iff, Rat.not_countably_generated_nhds_infty_opc, EReal.tendsto_coe_atBot, ENNReal.tendsto_toReal_zero_iff, ContDiffAt.exists_lipschitzOnWith_of_nnnorm_lt, IsCompact.nhdsSet_prod_eq_biSup, ENat.mem_nhds_natCast_iff, accPt_iff_frequently, HasDerivAt.tendsto_slope, Summable.tendsto_cofinite_zero, discreteTopology_iff_singleton_mem_nhds, ImplicitFunctionData.implicitFunction_apply_image, t1Space_iff_disjoint_pure_nhds, tendsto_logDeriv_euler_cot_sub, tendsto_norm', tendsto_inv_iff₀, Topology.isUpperSet_iff_nhds, uniformity_eq_comap_neg_add_nhds_zero, Complex.tendsto_partialGamma, Complex.exp_sub_sum_range_isBigO_pow, riemannZeta_eulerProduct, Topology.IsOpenEmbedding.tendsto_nhds_iff, tendsto_algebraMap_inverse_atTop_nhds_zero_nat, UpperHalfPlane.eventuallyEq_coe_comp_ofComplex, mem_closure_iff_ultrafilter, nhds_of_Ici_Iic, nhds_basis_Ioo', interior_eq_nhds', hasDerivAt_iff_isLittleO_nhds_zero, controlled_sum_of_mem_closure, eventually_norm_symmL_trivializationAt_lt, nhds_ofDual, ProperlyDiscontinuousVAdd.exists_nhds_disjoint_image, tendsto_nhds_of_eventually_eq, Asymptotics.isLittleO_iff_exists_eq_mul, UniformFun.hasBasis_nhds_one, tendsto_indicator_const_apply_iff_eventually, Metric.mem_nhds_iff, tendsto_zero_iff_norm_tendsto_zero, ContinuousAt.tendsto, nhdsSet_Ioc, Sigma.nhds_mk, MeasureTheory.tendsto_of_forall_isOpen_le_liminf_nat', ProbabilityTheory.Kernel.tendsto_setIntegral_densityProcess, eventuallyEq_nhds_of_eventuallyEq_nhdsNE, ENNReal.nhds_zero_basis_Iic, tendsto_atTop_iSup, indicator_cthickening_eventually_eq_indicator_closure, ContinuousMap.eventually_mapsTo, WeakBilin.tendsto_iff_forall_eval_tendsto, nhdsSet_Icc, ENat.nhds_natCast, HasStrictFDerivAt.eventually_right_inverse, IsTopologicalAddGroup.exist_add_closure_nhds, le_iff_nhds, tendsto_mod_div_atTop_nhds_zero_nat, UniformSpace.to_nhds_mono, uniformity_eq_comap_nhds_one_swapped, tendstoIccClassNhdsPi, numDerangements_tendsto_inv_e, MeasureTheory.tendsto_measure_iInter_atTop, MeasureTheory.tendsto_measure_Ici_atBot, Real.tendsto_of_bddBelow_antitone, AnalyticAt.exists_mem_nhds_analyticOnNhd, EMetric.mem_nhds_iff, ENNReal.tendsto_rpow_atTop_of_base_lt_one, comap_abs_nhds_zero, continuousWithinAt_iff_ptendsto_res, MeasureTheory.AECover.ae_tendsto_indicator, isLinearTopology_iff_hasBasis_open_ideal, AbsoluteValue.tendsto_div_one_add_pow_nhds_one, Real.tendsto_integral_cexp_sq_smul, tendsto_nat_ceil_div_atTop, Filter.nhds_mono, NormedAddCommGroup.tendsto_nhds_zero, WithSeminorms.tendsto_nhds_atTop, Real.zero_at_infty_fourier, map_snd_nhds, TopologicalSpace.ext_iff_nhds, HasFDerivAt.isBigO_sub, ZLattice.covolume.tendsto_card_le_div, tendsto_nhds, IsLUB.frequently_nhds_mem, pi_Iic_mem_nhds, tendsto_tsum_compl_atTop_zero, nhds_translation_sub, FiberBundle.map_proj_nhds, disjoint_pure_nhds, tendsto_conj_nhds_zero, nhds_basis_clopen, Asymptotics.superpolynomialDecay_iff_norm_tendsto_zero, mem_nhds_subtype_iff_nhdsWithin, properVAdd_iff_continuousVAdd_ultrafilter_tendsto, tendsto_atBot_iSup, isCobounded_le_nhds, lowerSemicontinuousAt_iff_le_liminf, GaussianFourier.tendsto_verticalIntegral, eventually_riemannianEDist_le_edist_extChartAt, ProbabilityTheory.strong_law_aux7, le_mem_nhds, ModuleFilterBasis.smul', nhds_basis_closed_balanced, ENNReal.tendsto_const_sub_nhds_zero_iff, tendsto_ceil_left', Continuous.integrableAt_nhds, Topology.IsUpperSet.nhds_eq_principal_Ici, Irrational.eventually_forall_le_dist_cast_div, AntitoneOn.tendsto_nhdsLT, AnalyticAt.analyticOrderAt_ne_top, tendsto_mul_prod_nhds_zero_of_disjoint_cocompact, tendsto_const_mul_zpow_atTop_zero, ProbabilityTheory.IsRatStieltjesPoint.tendsto_atTop_one, EulerSine.tendsto_integral_cos_pow_mul_div, nhdsWithin_pi_eq, UniformConvergenceCLM.hasBasis_nhds_zero, OpenPartialHomeomorph.eventually_nhds', PredOrder.hasBasis_nhds_Ioc, nhds_mul, ContDiffAt.contDiffOn, SimpleGraph.tendsto_turanDensity, MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess, ProbabilityTheory.Kernel.tendsto_densityProcess_limitProcess, CircleDeg1Lift.tendsto_translation_number₀, VectorField.mlieBracketWithin_eventually_congr_set', ENNReal.hasSum_iff_tendsto_nat, hasLineDerivAt_iff_tendsto_slope_zero, locallyConnectedSpace_iff_connected_basis, map_add_right_nhds_zero, IsUniformAddGroup.cauchy_iff_tendsto, ProbabilityTheory.strong_law_Lp, IsValuativeTopology.hasBasis_nhds', disjoint_nhds_atTop, eventually_le_nhds, ContinuousMap.tendsto_iff_tendstoLocallyUniformly, t2Space_iff_nhds, NumberField.Ideal.tendsto_norm_le_div_atTop, OnePoint.continuous_iff_from_discrete, ContractingWith.exists_fixedPoint', ENNReal.tendsto_nhds, Antitone.tendsto_nhdsLT, MeromorphicNFAt.eventuallyEq_nhdsNE_iff_eventuallyEq_nhds, compact_open_separated_mul_right, Asymptotics.isBigOTVS_iff, ContinuousMap.exists_tendsto_compactOpen_iff_forall, nhds_eq_uniformity, UniformSpace.mem_nhds_iff, IsCompact.inf_nhdsSet_eq_biSup, tendsto_div_comap_self, HasFPowerSeriesAt.eventually_hasSum_of_comp, nhds_def', Real.tendsto_logb_comp_add_sub_logb, IsUniformGroup.cauchy_iff_tendsto_swapped, tendsto_add, CompleteSpace.complete, ENNReal.tendsto_sub, Filter.tendsto_nhds_atTop_iff, uniformity_eq_comap_nhds_zero', EReal.tendsto_coe_nhds_top_iff, Filter.nhds_iInf, OpenPartialHomeomorph.eventually_right_inverse', MeasureTheory.SimpleFunc.tendsto_nearestPt, NNReal.nhds_zero, MeasureTheory.AECover.lintegral_tendsto_of_countably_generated, BoxIntegral.Integrable.tendsto_integralSum_toFilteriUnion_single, uniformity_eq_comap_neg_add_nhds_zero_swapped, Complex.Gammaℝ_residue_zero, eventually_nhdsWithin_iff, SeminormFamily.withSeminorms_iff_nhds_eq_iInf, Valued.mem_nhds_zero, Metric.disjoint_cobounded_nhds, eventually_ge_nhds, nhdsSet_diagonal, tendsto_norm, Ultrafilter.tendsto_pure_self, Real.tendsto_integral_exp_smul_cocompact, tendsto_closedBall_smallSets, nhdsAddHom_apply, Metric.nhds_basis_eball, tendsto_const_smul_iff₀, Filter.tendsto_const_div_iff', ENNReal.tendsto_sum_nat_add, nhds_induced, OnePoint.hasBasis_nhds_infty, Valued.mem_nhds, tendsto_rpow_div, eventually_mabs_div_lt, Asymptotics.IsEquivalent.tendsto_nhds_iff, MeasureTheory.eventually_nhds_one_measure_smul_diff_lt, egauge_eq_zero_iff, IsOpen.mem_nhds, LSeries.tendsto_cpow_mul_atTop, isOpen_singleton_iff_nhds_eq_pure, EisensteinSeries.tendsto_double_sum_S_act, OnePoint.continuousAt_infty', VitaliFamily.ae_tendsto_rnDeriv_of_absolutelyContinuous, eventually_nhds_subtype_iff, upperSemicontinuousAt_iff, WithTop.tendsto_untopD, HasStrictFDerivAt.isBigOTVS_sub, specializes_iff_nhds, Asymptotics.IsLittleOTVS.tendsto_inv_smul, tendsto_measure_cthickening_of_isClosed, ProbabilityTheory.IsRatStieltjesPoint.tendsto_atBot_zero, mem_tangentConeAt_iff_exists_seq, regularSpace_generateFrom, seminormFromConst_isLimit, UniformOnFun.hasBasis_nhds_of_basis, upperHemicontinuousAt_iff, MeasureTheory.tendsto_measure_iInter_atBot, MeasureTheory.tendstoInMeasure_iff_tendsto_toNNReal, MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos_ne_top, Specializes.pure_le_nhds, Monotone.tendsto_rightLim, tendsto_mul_add_inv_atTop_nhds_zero, HasFPowerSeriesAt.tendsto_partialSum, tendsto_indicator_const_iff_tendsto_pi_pure, tendstoLocallyUniformly_iff_forall_tendsto, MeasureTheory.TendstoInDistribution.tendsto, WithZeroTopology.singleton_mem_nhds_of_ne_zero, SmoothBumpCovering.eventuallyEq_one', EMetric.tendsto_nhdsWithin_nhds, HasFPowerSeriesAt.eventually_hasSum_sub, AnalyticAt.eventually_eq_or_eventually_ne, TendstoLocallyUniformlyOn.tendsto_comp, spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius, HasStrictFDerivAt.isThetaTVS_sub, nhds_eq_comap_uniformity', Filter.monotone_nhds, tendsto_nhds_of_tendsto_nhdsWithin, nhds_subtype_eq_comap_nhdsWithin, Filter.instIsCountablyGeneratedNhds, Metric.eventually_nhds_prod_iff, Ultrafilter.lim_eq_iff_le_nhds, MeasureTheory.StronglyMeasurable.tendsto_approx, MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat, nhds_mono, tendsto_atTop_ciInf, EMetric.nhds_basis_closed_eball, iteratedFDerivWithin_eventually_congr_set', tendsto_neg, uniformity_eq_comap_add_neg_nhds_zero_swapped, EReal.nhds_bot', NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one, tendsto_rpow_neg_div, ContinuousMap.tendsto_compactOpen_iff_forall, Uniform.continuous_iff'_right, VitaliFamily.ae_tendsto_rnDeriv, AnalyticAt.eventually_eq_zero_or_eventually_ne_zero, Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero, ContinuousLinearMap.nhds_zero_eq, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, tendsto_mul, SeminormedGroup.disjoint_nhds_one, tendsto_rpow_neg_atTop, LSeries.tendsto_atTop, ProbabilityTheory.Kernel.tendsto_densityProcess_fst_atTop_ae_of_monotone, ENNReal.tendsto_rpow_atBot_of_one_lt_base, PointwiseConvergenceCLM.tendsto_nhds_atTop, regularSpace_iff, Continuous.tendstoUniformly, HasFPowerSeriesOnBall.eventually_hasSum_sub, map_mul_right_nhds₀, isLinearTopology_iff_hasBasis_open_submodule, Dense.comap_val_nhds_neBot, Polynomial.div_tendsto_atBot_zero_iff_degree_lt, DomAddAct.map_mk_nhds, GroupFilterBasis.nhds_eq, Dense.exists_seq_strictAnti_tendsto, tendsto_mulIndicator_thickening_mulIndicator_closure, Asymptotics.isEquivalent_iff_tendsto_one, NNReal.tendsto_inverse_atTop_nhds_zero_nat, EReal.tendsto_nhds_top_iff_real, EReal.nhds_bot, NormedCommGroup.nhds_basis_norm_lt, zero_at_infty_of_norm_le, MulOpposite.map_unop_nhds, hasBasis_nhds_closure, MeasureTheory.Submartingale.ae_tendsto_limitProcess, BumpCovering.eventuallyEq_one', equicontinuousAt_iff_pair, WithTop.tendsto_coe_atTop, Metric.eventually_notMem_cthickening_of_infEdist_pos, tendsto_sub_mul_tsum_nat_rpow, MulOpposite.comap_op_nhds, Sigma.nhds_eq, Dense.extend_spec, MvPowerSeries.WithPiTopology.tendsto_trunc'_atTop, tendsto_indicator_cthickening_indicator_closure, ProbabilityTheory.tendsto_cdf_atTop, Complex.UnitDisc.tendsto_pow_atTop_nhds_zero, MeasureTheory.exists_null_frontiers_thickening, LaurentSeries.tendsto_valuation, Real.BohrMollerup.tendsto_logGammaSeq, MeasureTheory.tendsto_measure_of_ae_tendsto_indicator, MeasureTheory.Measure.tendsto_IicSnd_atTop, tendsto_pow_atTop_nhds_zero_of_lt_one, Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO, Real.tendsto_sum_pi_div_four, LocallyConvexSpace.convex_open_basis_zero, uniformity_eq_comap_nhds_zero_swapped, EMetric.nhds_eq, uniformly_extend_exists, nhds_nhdsAdjoint_same, UniformOnFun.gen_mem_nhds, tendsto_iff_edist_tendsto_0, krullTopology_mem_nhds_one_iff, ENNReal.tendsto_nhds_coe_iff, Real.tendsto_div_pow_mul_exp_add_atTop, MeasureTheory.tendsto_diracProbaEquivSymm_iff_tendsto, specializes_iff_not_disjoint, Asymptotics.isLittleOTVS_iff_tendsto_inv_smul, Metric.eventually_notMem_thickening_of_infEdist_pos, specializes_iff_pure, TotallyBounded.nhds_vietoris_le_nhds_hausdorff, tendsto_pow_const_mul_const_pow_of_lt_one, IsLocalHomeomorph.map_nhds_eq, Filter.Germ.sliceLeft_coe, Metric.eventually_nhds_iff_ball, OrderTop.tendsto_atTop_nhds, MeasureTheory.Submartingale.exists_ae_tendsto_of_bdd, bernsteinApproximation_uniform, Uniform.continuousAt_iff'_right, NormedRing.inverse_add_norm_diff_first_order, isOpen_isPathConnected_basis, disjoint_nhds_pure, Ici_mem_nhds, Asymptotics.isLittleO_norm_pow_id, tendsto_atTop_nhds, nhds_one_symm, Polynomial.div_tendsto_atTop_zero_of_degree_lt, SmoothBumpFunction.eventuallyEq_one_of_dist_lt, MeasureTheory.tendsto_of_forall_isOpen_le_liminf, tendsto_one_iff_norm_tendsto_zero, Metric.uniformity_eq_comap_nhds_zero, map_mul_right_nhds_one₀, IsUniformAddGroup.cauchy_map_iff_tendsto_swapped, krullTopology_mem_nhds_one_iff_of_normal, MeasureTheory.exists_seq_tendstoInMeasure_atTop_iff, ContinuousMap.tendsto_of_tendstoLocallyUniformly, nhds_le_nhds_iff, tendsto_atBot_isGLB, tendsto_measure_Icc_nhdsWithin_right', Real.tendsto_eulerMascheroniSeq, Metric.eventually_notMem_cthickening_of_infEDist_pos, PointwiseConvergenceCLM.tendsto_iff_forall_tendsto, BumpCovering.exists_finset_toPOUFun_eventuallyEq, tendsto_const_mul_zpow_atTop_nhds_iff, HasFPowerSeriesOnBall.eventually_eq_zero, Polynomial.div_tendsto_zero_of_degree_lt, contDiffAt_zero, OpenPartialHomeomorph.map_extend_nhds_of_mem_interior_range, Multipliable.tendsto_prod_tprod_nat, ContinuousMap.tendsto_nhds_compactOpen, ImplicitFunctionData.right_map_implicitFunction, nhds_list, WithZeroTopology.tendsto_units, ContDiffAt.laplacian_CLM_comp_left_nhds, isSeparatedMap_iff_nhds, AffineSpace.asymptoticNhds_eq_smul, exists_seq_strictMono_tendsto, WithZeroTopology.Iio_mem_nhds_zero, ENNReal.tendsto_atTop_zero, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, Inseparable.nhds_le_uniformity, eventuallyEq_toIocDiv_nhds, tendsto_div_nhds_one_iff, interior_mem_nhds, tendsto_nat_ceil_mul_div_atTop, Complex.arg_eq_nhds_of_im_pos, Icc_mem_nhds_iff, ContDiffBump.eventuallyEq_one_of_mem_ball, eventuallyConst_iff_analyticOrderAt_sub_eq_top, tendsto_atTop_iInf, properSMul_iff_continuousSMul_ultrafilter_tendsto, nhds_eq_comap_uniformity, Asymptotics.isLittleO_one_iff, ContDiffAt.exists_eventually_eq_hasDerivAt, Hyperreal.isSt_iff_tendsto, nhds_prod_eq, hasFDerivAtFilter_iff_tendsto, AbsoluteValue.tendsto_div_one_add_pow_nhds_zero, Complex.log_sub_logTaylor_isBigO, Filter.IsApproximateUnit.tendsto_mul_right, IsAddFoelner.tendsto_nhds_mean, spectrum.resolvent_tendsto_cobounded, ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection, MeasureTheory.tendsto_of_forall_isOpen_le_liminf', AddOpposite.map_unop_nhds, HasDerivAt.tendsto_slope_zero, intervalIntegral.FTCFilter.nhds, gc_nhds, Function.Periodic.tendsto_at_I_inf, NormedAddCommGroup.tendsto_atTop, Real.tendsto_pow_logb_div_mul_add_atTop, MeasureTheory.Egorov.measure_notConvergentSeq_tendsto_zero, NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero, Topology.isLowerSet_iff_nhds, cpow_eq_nhds', Filter.Tendsto.const_div_atTop, Real.rpow_eq_nhds_of_pos, ContinuousAt.eventually_ne, Euclidean.closedBall_mem_nhds, EReal.tendsto_toReal, Complex.isOpen_setOf_mem_nhds_and_isMaxOn_norm, MeasureTheory.tendsto_setIntegral_of_monotone, Metric.eventually_notMem_thickening_of_infEDist_pos, nhdsLE_sup_nhdsGT, ContinuousAt.nhds, disjoint_lift'_closure_nhds, tendsto_subtype_rng, nhds_zero_symm', MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm', tendsto_sum_nat_add, MeasureTheory.tendsto_measure_iUnion_accumulate, HasStrictFDerivAt.isTheta_sub, IsGLB.exists_seq_antitone_tendsto, HasFPowerSeriesAt.isBigO_sub_partialSum_pow, nhds_basis_Ioo, Asymptotics.isLittleO_id_const, nhds_inv, ProbabilityTheory.strong_law_ae_simpleFunc_comp, absorbs_iff_eventually_nhds_zero, QuotientAddGroup.nhds_eq, UniformConvergenceCLM.tendsto_iff_tendstoUniformlyOn, AntilipschitzWith.comap_nhds_le, isMIntegralCurveAt_eventuallyEq_of_contMDiffAt, Real.tendsto_integral_gaussian_smul, Convex.diff_singleton_eventually_mem_nhds, IsLocalMaxOn.not_nhds_le_map, Ico_mem_nhds, isOpen_iff_mem_nhds, tendsto_fib_succ_div_fib_atTop, tendsto_measure_cthickening_of_isCompact, ENNReal.tendsto_nhds_zero, OpenPartialHomeomorph.isBigOWith_congr, Asymptotics.isLittleOTVS_iff, Metric.nhds_basis_ball_inv_nat_succ, tendsto_nhds_of_unique_mapClusterPt, AddMonoidHom.exists_nhds_isBounded, PowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent, tendsto_integral_exp_inner_smul_cocompact, EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq, IsUniformGroup.ext_iff, isLinearTopology_iff_hasBasis_submodule, UniformOnFun.hasBasis_nhds_zero, IsBoundedLinearMap.tendsto, isCompact_iff_ultrafilter_le_nhds', nhds_translation_neg_add, mem_nhds_iff_exists_Ioo_subset, Complex.arg_eq_nhds_of_re_pos, limsInf_nhds, ConcaveOn.continuousOn_tfae, LocPathConnectedSpace.path_connected_basis, Asymptotics.isLittleO_iff_tendsto, LocallyConvexSpace.convex_basis, IsContDiffImplicitAt.comp_implicitFunctionAux_eq_snd, tendsto_inv, PointwiseConvergenceCLM.hasBasis_nhds_zero, MeasureTheory.tendsto_measure_compl_closedBall_of_isTightMeasureSet, IsAddFoelner.tendsto_meas_vadd_symmDiff, map_add_left_nhds, exists_mem_nhds_isCompact_isClosed, NNReal.tendsto_coe, Metric.nhds_basis_ball, nhds_isMeasurablyGenerated, ptendsto'_nhds, Metric.nhds_basis_closedEBall, MeasureTheory.tendstoInMeasure_iff_enorm, MeasureTheory.StronglyMeasurable.stronglyMeasurable_in_set, Ioc_mem_nhds, ZLattice.covolume.tendsto_card_le_div'', nhds_discrete, map_fst_nhds, nhds_eq_uniformity', tendsto_neg_iff, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atTop_one, tendsto_pow_const_div_const_pow_of_one_lt, LocallyConnectedSpace.open_connected_basis, isOpen_iff_nhds, DirichletCharacter.LFunctionTrivChar_residue_one, IsCompact.nhdsSet_inf_eq_biSup, pure_sup_nhdsNE, List.Vector.tendsto_insertIdx, UniformOnFun.hasBasis_nhds_one, TrivSqZeroExt.nhds_inr, r1Space_iff_specializes_or_disjoint_nhds, ImplicitFunctionData.prod_map_implicitFunction, nhds_bot_order, tendsto_inv₀, AnalyticAt.eventually_analyticAt, WithZeroTopology.tendsto_zero, EReal.nhds_top, tendsto_atTop_of_antitone, pi_Ici_mem_nhds, OnePoint.nhds_infty_eq, IsLinearTopology.hasBasis_ideal, completedRiemannZeta_residue_one, tendsto_of_monotone, ContinuousOn.tendsto_restrict_iff_tendstoUniformlyOn, Filter.nhds_nhds, Continuous.tendsto', NormedAddCommGroup.nhds_zero_basis_norm_lt, ContinuousLinearEquiv.map_nhds_eq, clusterPt_iff_ultrafilter, Metric.nhds_basis_closedBall, nhds_eq_uniformity_prod, Filter.EventuallyEq.tendsto, set_pi_mem_nhds_iff, IsTopologicalGroup.exist_mul_closure_nhds, tendsto_card_div_pow_atTop_volume', MeasureTheory.tendsto_measure_of_le_liminf_measure_of_limsup_measure_le, MeasureTheory.tendsto_Lp_finite_of_tendstoInMeasure, CircleDeg1Lift.tendsto_translationNumber, uniformly_extend_spec, BoxIntegral.Integrable.tendsto_integralSum_sum_integral, Filter.Tendsto.inv_tendsto_atTop, ProbabilityTheory.strong_law_ae_real, EReal.tendsto_mul, MeasureTheory.tendsto_measure_smul_diff_isCompact_isClosed, SmoothPartitionOfUnity.eventually_finsupport_subset, Real.tendsto_euler_sin_prod, Filter.tendsto_nhds_atTop, MeasureTheory.tendsto_setToFun_approxOn_of_measurable, eventually_eventually_nhds, IsLUB.exists_seq_monotone_tendsto, LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul, MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero, Filter.tendsto_div_const_iff', tendsto_inverse_atTop_nhds_zero_nat, ZeroAtInftyContinuousMap.tendsto_iff_tendstoUniformly, Complex.arg_eq_nhds_of_re_neg_of_im_pos, InnerProductSpace.laplacian_smul_nhds, NNReal.tendsto_coe', WithTop.tendsto_nhds_top_iff, MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt, WithIdealFilter.mem_nhds_iff, IsLUB.exists_seq_strictMono_tendsto_of_notMem, AffineSpace.asymptoticNhds_eq_smul_vadd, MeasureTheory.Measure.tendsto_IicSnd_atBot, tendsto_seminormFromConst_seq_atTop, insert_mem_nhds_iff, NNReal.nhds_zero_basis, IsCompact.nhds_hausdorff_eq_nhds_vietoris, ENNReal.tendsto_nhds_top_iff_nat, exists_seq_tendsto_sInf, pi_Ioc_mem_nhds', OnePoint.ultrafilter_le_nhds_infty, TopologicalSpace.nhds_mkOfNhds_filterBasis, IsCompact.ultrafilter_le_nhds, frequently_nhdsWithin_iff, alexandrovDiscrete_iff_nhds, ZMod.LFunction_residue_one, MvPowerSeries.WithPiTopology.variables_tendsto_zero, tendsto_left_nhds_uniformity, ENNReal.nhds_top, UniformOnFun.hasBasis_nhds, vadd_mem_nhds_vadd_iff, ModuleFilterBasis.smul, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, map_nhds_induced_eq, tendsto_of_le_liminf_of_limsup_le, cpow_eq_nhds, hasGradientWithinAt_iff_tendsto, ContractingWith.tendsto_iterate_efixedPoint', ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atTop, ContinuousMap.eventually_range_subset, IsLinearTopology.hasBasis_subbimodule, Complex.tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero, ultrafilter_converges_iff, HasCompactSupport.is_zero_at_infty, ContinuousMap.nhds_compactOpen, OnePoint.tendsto_nhds_infty', nhds_basis_opens, AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_iff, Real.tendsto_sin_pi_div_two, Filter.Tendsto.nhds_atTop, hasDerivAt_iff_tendsto, Filter.Tendsto.const_div_atBot, riemannZeta_residue_one, Trivialization.nhds_eq_inf_comap, ENNReal.biInf_le_nhds, continuousAt_def, mem_tangentConeAt_iff_exists_seq_norm_tendsto_atTop, nhds_bot_basis_Iic, Filter.nhds_atTop, LocallyFinite.exists_finset_nhds_mulSupport_subset, pi_Icc_mem_nhds, RestrictedProduct.nhds_zero_eq_map_structureMap, PadicInt.continuousAddCharEquiv_apply, SummationFilter.hasProd_symmetricIcc_iff, NNReal.tendsto_tsum_compl_atTop_zero, nhds_top_basis, OpenPartialHomeomorph.tendsto_symm, clusterPt_principal_iff_frequently, Complex.IsConservativeOn.eventually_nhds_wedgeIntegral_sub_wedgeIntegral, inf_nhds_atBot, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_restrict_densityProcess_limitProcess, OnePoint.tendsto_coe_infty, locallyConvexSpace_iff_zero, Irrational.eventually_forall_le_dist_cast_rat_of_den_le, tendsto_of_no_upcrossings, IsUniformGroup.cauchy_iff_tendsto, continuousWithinAt_update_same, mulIndicator_cthickening_eventually_eq_mulIndicator_closure, pi_Ioi_mem_nhds, ContinuousOn.nhds, ENat.tendsto_nhds_top_iff_natCast_lt, EReal.nhds_coe_coe, OpenPartialHomeomorph.map_nhds_eq, pairwise_disjoint_nhds, HurwitzZeta.completedHurwitzZetaEven_residue_zero, NormedRing.inverse_add_nth_order, cauchy_nhds, ProbabilityTheory.strong_law_ae_of_measurable, PowerSeries.WithPiTopology.tendsto_trunc_atTop, tendsto_atTop_isLUB, Real.tendsto_log_nat_add_one_sub_log, HurwitzZeta.tendsto_hurwitzZeta_sub_one_div_nhds_one, OpenPartialHomeomorph.map_extend_symm_nhdsWithin_range, nhdsWithin_pi_eq', ultrafilter_comap_pure_nhds, disjoint_nhds_atTop_iff, Real.zero_at_infty_vector_fourierIntegral, Summable.tendsto_zero_of_even_summable_symmetricIcc, HasFPowerSeriesWithinOnBall.tendsto_partialSum, tendsto_atTop_of_monotone, nhdsLE_sup_nhdsGE, IsCompact.disjoint_nhdsSet_right, mem_nhds_iff_exists_Ioo_subset', Topology.IsClosedEmbedding.tendsto_nhds_iff, lift_nhds_left, Polynomial.tendsto_div_exp_atTop, nhds_basis_nhdsKer_singleton, Complex.arg_eq_nhds_of_re_neg_of_im_neg, EMetric.eventually_nhds_zero_forall_closedBall_subset, IsUniformGroup.cauchy_map_iff_tendsto_swapped, ENNReal.tendsto_toReal_iff, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_monotone, TopologicalSpace.IsTopologicalBasis.mem_nhds_iff, ContinuousWithinAt.tendsto, Real.tendsto_pow_log_div_mul_add_atTop, ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE, tendsto_smoothingFun_of_eq_zero, Filter.continuous_nhds, MeasureTheory.SimpleFunc.tendsto_approxOn_L1_enorm, Dense.exists_seq_strictMono_tendsto_of_lt, OpenPartialHomeomorph.nhds_eq_comap_inf_principal, ultrafilter_extend_eq_iff, IsOpenMap.range_mem_nhds, tendsto_nhds_true, Stirling.tendsto_stirlingSeq_sqrt_pi, Valued.loc_const, MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto, nhdsSet_singleton, TopologicalGroup.isOpenMap_iff_nhds_zero, Dense.exists_seq_strictMono_tendsto, VitaliFamily.ae_tendsto_limRatioMeas, unitInterval.tendsto_sigmoid_atBot, le_nhds_of_unique_clusterPt, disjoint_nested_nhds, PartitionOfUnity.exists_finset_nhds', NormedCommGroup.tendsto_nhds_one, tendsto_norm_zero, MeasureTheory.Submartingale.exists_ae_trim_tendsto_of_bdd, Topology.IsLowerSet.nhds_eq_principal_Iic, WithZeroTopology.singleton_mem_nhds_of_units, OnePoint.le_nhds_infty, HasFPowerSeriesAt.locally_zero_iff, hasDerivAt_iff_tendsto_slope, MeasureTheory.tendsto_iff_forall_lipschitz_integral_tendsto, MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi, disjoint_nhdsSet_nhds, eventually_norm_trivializationAt_lt, nhds_ofAdd, SeparationQuotient.map_prod_map_mk_nhds, WithSeminorms.hasBasis, ENNReal.tendsto_ofReal_nhds_top, AddGroupFilterBasis.mem_nhds_zero, UniformConvergenceCLM.nhds_zero_eq, VitaliFamily.ae_tendsto_average, Homeomorph.symm_map_nhds_eq, tendsto_algebraMap_inv_atTop_nhds_zero_nat, MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat, pi_Ioo_mem_nhds', pi_Icc_mem_nhds', Filter.sInter_nhds, LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul', tendsto_const_div_pow, Asymptotics.isLittleO_pow_sub_sub, Filter.IsApproximateUnit.iff_neBot_and_le_nhds_one, extChartAt_target_eventuallyEq_of_mem, tendsto_euler_sin_prod', NonarchimedeanGroup.multipliable_iff_tendsto_cofinite_one, nhds_bind_nhdsWithin, exists_continuousLinearEquiv_fderiv_symm_eq, map_mul_left_nhds₀, exists_seq_strictMono_tendsto', SmoothBumpFunction.eventuallyEq_one, AnalyticAt.frequently_eq_iff_eventually_eq, UniformOnFun.nhds_eq, Metric.nhds_basis_ball_inv_nat_pos, MeasureTheory.tendsto_measure_Ico_atTop, extChartAt_target_mem_nhds, tendsto_subseq_of_bounded, hasFDerivWithinAt_iff_tendsto, nhds_toDual, MeasureTheory.isTightMeasureSet_iff_tendsto_measure_compl_closedBall, tendsto_comp_of_locally_uniform_limit_within, tendsto_log_mul_rpow_nhdsGT_zero, tendsto_const_nhds_iff, tendsto_floor_right', IsValuativeTopology.mem_nhds_iff, nhdsSet_Ico, hasSum_iff_tendsto_nat_of_nonneg, MeasureTheory.tendsto_integral_norm_approxOn_sub, ENNReal.tendsto_rpow_atBot_of_base_lt_one, closure_image_mem_nhds_of_isUniformInducing, compact_open_separated_add_left, ZLattice.covolume.tendsto_card_div_pow'', nhds_basis_mabs_div_lt, tendsto_pow_atTop_nhds_zero_of_norm_lt_one, hasDerivWithinAt_iff_tendsto_slope', MeasureTheory.tendsto_measure_of_null_frontier, lift'_nhds_interior, DirichletCharacter.LSeries_eulerProduct, InfConvergenceClass.tendsto_coe_atBot_isGLB, SeminormedAddGroup.disjoint_nhds, tendsto_mulIndicator_cthickening_mulIndicator_closure, IsCompact.disjoint_nhdsSet_nhds, DenseRange.exists_seq_strictAnti_tendsto_of_lt, lowerSemicontinuousAt_iff, range_mem_nhds_isInteriorPoint, TopologicalSpace.IsTopologicalBasis.nhds_hasBasis, Metric.tendstoLocallyUniformly_iff, ENNReal.tendsto_nhds_top, MeasureTheory.tendsto_of_forall_isOpen_le_liminf_nat, tendsto_measure_thickening_of_isClosed, ENNReal.tendsto_coe_nhds_top, tendsto_pow_atTop_nhds_zero_iff, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn, ker_nhds, Uniform.continuous_iff'_left, tendsto_iff_dist_tendsto_zero, lift_nhds_right, nhds_basis_uniformity, Asymptotics.isEquivalent_const_iff_tendsto, Polynomial.div_tendsto_atTop_zero_iff_degree_lt, eventually_nhdsSet_iff_forall, extChartAt_preimage_mem_nhds_of_mem_nhdsWithin, MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint, tendsto_atBot_iInf, tendsto_factorial_div_pow_self_atTop, isLinearTopology_iff_hasBasis_twoSidedIdeal, CompactSpace.tendsto_subseq, Filter.tendsto_mul_const_iff, PowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero, MeasureTheory.tendsto_of_forall_isClosed_limsup_le', nhds_translation_inv_mul, nhds_translation_div, OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq, LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure, VitaliFamily.ae_tendsto_lintegral_enorm_sub_div_of_integrable, UniformSpace.hasBasis_nhds_prod, NNReal.tendsto_const_div_atTop_nhds_zero_nat, Asymptotics.IsLittleO.exists_eq_mul, WithZeroTopology.nhds_eq_update, tendsto_nhds_of_meromorphicOrderAt_nonneg, Metric.eventually_isCompact_closedBall, hasDerivWithinAt_iff_tendsto_slope, map_mul_left_nhds_one, VitaliFamily.ae_tendsto_lintegral_enorm_sub_div, SeparationQuotient.map_mk_nhds, mem_nhdsWithin_iff_exists_mem_nhds_inter, tendsto_tprod_compl_atTop_one, ENNReal.Icc_mem_nhds, Real.tendsto_prod_pi_div_two, ContDiffPointwiseHolderAt.zero_order_iff, Real.exp_sub_sum_range_isBigO_pow, VitaliFamily.ae_tendsto_lintegral_enorm_sub_div'_of_integrable, WeakFEPair.Λ_residue_zero, OnePoint.continuous_iff_from_nat, Ctop.Realizer.tendsto_nhds_iff, ContDiffAt.exists_lipschitzOnWith, Filter.tendsto_const_div_iff, Complex.approx_Gamma_integral_tendsto_Gamma_integral, Topology.IsEmbedding.map_nhds_eq, NormedAddCommGroup.tendsto_atTop', NNReal.tendsto_cofinite_zero_of_summable, IsLocalHomeomorph.exists_lift_nhds, eventually_norm_mfderiv_extChartAt_lt, IsDiscrete.exists_nhds_eq_zero_of_image_addRight_inter_nonempty, IsFoelner.tendsto_nhds_mean, Real.BohrMollerup.tendsto_logGammaSeq_of_le_one, tendsto_norm_sub_self_nhdsGE, Monotone.tendsto_nhdsGT, BoundedContinuousFunction.tendsto_iff_tendstoUniformly, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp_finite, mem_nhds_right, Uniform.tendsto_nhds_left, MeasureTheory.tendsto_integral_meas_thickening_le, ContinuousLinearEquiv.symm_map_nhds_eq, SummationFilter.hasProd_symmetricIoc_int_iff, MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic, Real.tendsto_one_add_div_rpow_exp, MvPowerSeries.HasEval.tendsto_zero, tendsto_log_mul_self_nhdsLT_zero, Set.ordConnectedComponent_mem_nhds, BoundedContinuousFunction.tendsto_integral_of_forall_limsup_integral_le_integral, Specializes.not_disjoint, tendsto_indicator_thickening_indicator_closure, LocallyFinite.eventually_smallSets, uniformity_eq_comap_nhds_one', hasFPowerSeriesAt_iff', SmoothBumpFunction.nhds_basis_tsupport, TopologicalSpace.nhds_mkOfNhds, ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto, isAddFoelner_iff, Homeomorph.isLittleO_congr, WeakFEPair.Λ_residue_k, WithSeminorms.hasBasis_ball, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm, Complex.analyticAt_iff_eventually_differentiableAt, Ordinal.nhds_eq_pure, ImplicitFunctionData.left_map_implicitFunction, notMem_mulTSupport_iff_eventuallyEq, tendstoLocallyUniformly_iff_filter, HasOuterApproxClosed.exAppr, locallyConnectedSpace_iff_hasBasis_isOpen_isConnected, IsCompact.le_nhds_of_unique_clusterPt, Monotone.tendsto_leftLim, Manifold.exists_lt_locally_constant_of_riemannianEDist_lt, UniformFun.hasBasis_nhds_of_basis, ProbabilityTheory.tendsto_cdf_atBot, Real.tendsto_harmonic_sub_log_add_one, uniformity_eq_comap_nhds_one, ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_nhds_right, continuousAt_update_same, Ideal.hasBasis_nhds_adic, ProbabilityTheory.tendsto_condCDF_atTop, ModuleFilterBasis.smul_right', le_nhds_mul, tendsto_inv_atTop_nhds_zero_nat, isAddQuotientCoveringMap_iff, Function.IsFixedPt.tendsto_birkhoffAverage, MvPowerSeries.LinearTopology.hasBasis_nhds_zero, IsLocalHomeomorphOn.map_nhds_eq, tendsto_subseq_of_frequently_bounded, lt_mem_nhds, hasFDerivAt_iff_isLittleO_nhds_zero, MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm, isBounded_le_nhds, nhds_one_mul_nhds, HasFiniteFPowerSeriesAt.eventually_const_of_bound_one, ContDiffAt.eventually, WithTop.nhds_coe, pure_le_nhds_iff, Filter.tendsto_const_sub_iff, Real.exists_seq_rat_strictMono_tendsto, MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae', isLocallyInjective_iff_nhds, Dense.extend_exists, EMetric.ball_mem_nhds, ContinuousOn.stronglyMeasurableAtFilter, hasDerivWithinAt_iff_tendsto, disjoint_nhds_atBot, CircleDeg1Lift.tendsto_translation_number₀', AffineSpace.asymptoticNhds_bind_nhds, discreteTopology_iff_nhds, uniformity_eq_comap_inv_mul_nhds_one_swapped, Metric.nhds_basis_ball_pow, Topology.IsOpenEmbedding.tendsto_nhds_iff', tendsto_sub_nhds_zero_iff, CircleDeg1Lift.tendsto_translationNumber_of_dist_bounded_aux, IsLinearTopology.hasBasis_open_twoSidedIdeal, FirstCountableTopology.nhds_generated_countable, hasFPowerSeriesAt_iff, map_extChartAt_nhds, HasStrictFDerivAt.eq_implicitFunction, MeasureTheory.StronglyMeasurable.tendsto_approxBounded_of_norm_le, specializes_TFAE, upperHemicontinuous_iff_forall_isOpen, UpperSemicontinuous.limsup_le, HasStrictDerivAt.eventually_left_inverse, DomAddAct.comap_mk_nhds, IsContDiffImplicitAt.implicitFunctionAux_fst, Asymptotics.superpolynomialDecay_iff_abs_tendsto_zero, ProbabilityTheory.Kernel.tendsto_density_fst_atTop_ae_of_monotone, NormedAddCommGroup.nhds_basis_norm_lt, Iic_mem_nhds, MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto, IsCompact.tendsto_nhds_of_unique_mapClusterPt, Submodule.starProjection_tendsto_closure_iSup, map_add_left_nhds_zero, rtendsto_nhds, IsLinearTopology.hasBasis_right_ideal, tendstoIooClassNhds, DenseRange.exists_seq_strictAnti_tendsto, Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici, Uniform.continuousAt_iff_prod, EReal.mem_nhds_top_iff, MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto, nhdsNE_sup_pure, map_nhds_subtype_val, ProbabilityTheory.IsMeasurableRatCDF.tendsto_stieltjesFunction_atBot, MeasureTheory.AECover.lintegral_tendsto_of_nat, MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_rclike_tendsto, nhds_smul, IsDiscrete.exists_nhds_eq_one_of_image_mulLeft_inter_nonempty, eventually_riemannianEDist_lt, Real.tendsto_mulExpNegMulSq, IsMIntegralCurveAt.eventually_hasDerivAt, LocallyFinite.eventually_subset, AntitoneOn.tendsto_nhdsWithin_Ioo_left, MeasureTheory.Lp.cauchy_complete_eLpNorm, Complex.isEquivalent_sin, nhds_toMul, Filter.Tendsto.inv_tendsto_atBot, IsDenseInducing.tendsto_extend, ENNReal.nhds_coe_coe, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm, HasDerivAt.tendsto_slope_zero_right, ENNReal.tendsto_nhds_of_Icc, Real.BohrMollerup.tendsto_log_gamma, extChartAt_target_mem_nhds', nhds_le_nhdsSet_iff, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto, Real.tendsto_one_add_div_pow_exp, WithSeminorms.hasBasis_zero_ball, AnalyticAt.eventually_continuousAt, ProbabilityTheory.IsMeasurableRatCDF.tendsto_atTop_one, Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero, NNReal.tendsto_pow_atTop_nhds_zero_iff, Asymptotics.IsTheta.tendsto_zero_iff, IsCompact.tendsto_subseq, tendsto_inf_principal_nhds_iff_of_forall_eq, UniformFun.hasBasis_nhds, locallyConvexSpace_iff_exists_convex_subset_zero, HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt, Hyperreal.isSt_ofSeq_iff_tendsto, RestrictedProduct.nhds_eq_map_inclusion, Stirling.tendsto_self_div_two_mul_self_add_one, IsTopologicalAddGroup.tendstoLocallyUniformly_iff, Stirling.stirlingSeq_has_pos_limit_a, uniformity_eq_comap_nhds_one_left, WithZeroTopology.hasBasis_nhds_units, le_nhds_of_limsSup_eq_limsInf, EReal.tendsto_nhds_bot_iff_real, nhdsMulHom_apply, Filter.tendsto_pure_self, Icc_mem_nhds, Trivialization.map_proj_nhds, disjoint_nhds_nhds, NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat, TopologicalSpace.IsOpenCover.exists_mem_nhds, tendsto_iff_norm_sub_tendsto_zero, Real.isEquivalent_sinh, IsLinearTopology.hasBasis_open_subbimodule, Topology.IsUpper.tendsto_nhds_iff_lt, HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto, tendsto_mul_nhds_zero_prod_of_disjoint_cocompact, tendsto_prod_principal_iff, tendsto_rpow_atBot_of_base_gt_one, Asymptotics.isBigO_one_nhds_ne_iff, LinearOrderedAddCommGroup.tendsto_nhds, OpenPartialHomeomorph.eventually_nhds, Topology.IsInducing.map_nhds_eq, continuous_iff_ultrafilter, map_mul_right_nhds, controlled_prod_of_mem_closure, tendsto_prod_nat_add, IsTopologicalGroup.isInducing_iff_nhds_one, HurwitzZeta.hurwitzZetaEven_residue_one, tendsto_zero_geometric_tsum_pnat, limsSup_nhds, lim_nhds, NormedAddCommGroup.summable_imp_tendsto_of_complete, locallyConvexSpace_iff_exists_convex_subset, tendsto_right_nhds_uniformity, isCompactOperator_iff_exists_mem_nhds_image_subset_compact, isComplete_iff_ultrafilter', Real.tendsto_logb_nat_add_one_sub_logb, Urysohns.CU.tendsto_approx_atTop, List.tendsto_cons, AddOpposite.map_op_nhds, ProbabilityTheory.Kernel.tendsto_densityProcess_atTop_of_antitone, continuous_nhdsAdjoint_dom
nhdsKer 📖	CompOp	52 math math: nhdsKer_subset_nhdsKer_iff_nhdsSet, nhdsKer_inter_subset, nhdsKer_subset_iff_mem_nhdsSet, subset_nhdsKer_iff, Topology.IsUpperSet.nhdsKer_eq_upperClosure, Topology.IsLowerSet.nhdsKer_eq_lowerClosure, nhdsKer_iInter_subset, nhdsKer_singleton_eq_ker_nhds, subset_nhdsKer, IsOpen.nhdsKer_subset, nhdsKer_singleton_pi, principal_nhdsKer_singleton, mem_nhdsKer_iff_specializes, nhdsKer_eq_nhdsKer_iff_nhdsSet, nhdsKer_nhdsKer, nhdsKer_union, nhdsKer_singleton_subset_iff_mem_nhds, nhdsKer_subset_iff, nhdsSet_basis_nhdsKer, nhdsKer_pair, gc_nhdsKer_interior, Topology.IsLowerSet.nhdsKer_singleton, nhdsKer_prod, specializes_iff_nhdsKer_subset, nhdsKer_pi, IsOpen.nhdsKer_eq, nhdsKer_subset_nhdsKer, nhdsKer_univ, nhdsKer_eq_iff_isOpen, nhdsKer_def, IsCompact.closure_eq_nhdsKer, IsCompact.nhdsKer, nhdsKer_biUnion, isOpen_nhdsKer, Topology.IsUpperSet.nhdsKer_singleton, nhdsKer_sInter_subset, principal_nhdsKer, nhdsKer_mem_nhdsSet, alexandrovDiscrete_iff_nhds, nhdsKer_subset_iff_isOpen, nhds_basis_nhdsKer_singleton, nhdsKer_mono, mem_nhdsKer_singleton, nhdsKer_sUnion, nhdsKer_empty, mem_nhdsKer, nhdsKer_minimal, nhdsSet_nhdsKer, nhdsKer_iUnion, nhdsKer_eq_empty, nhdsKer_eq_of_t1Space, IsCompact.nhdsKer_iff
nhdsSet 📖	CompOp	174 math math: nhdsKer_subset_nhdsKer_iff_nhdsSet, nhdsSet_insert, nhdsKer_subset_iff_mem_nhdsSet, mem_nhdsSet_subtype_iff_nhdsSetWithin, Continuous.tendsto_nhdsSet_nhds, prod_nhds_le_of_disjoint_cocompact, nhdsSet_Ioo, nhds_le_nhdsSet, strictMono_nhdsSet, mem_nhdsSet_empty, SeparationQuotient.map_mk_nhdsSet, nhdsSet_union, exists_smooth_one_nhds_of_subset_interior, IsClosedMap.comap_nhds_eq, IsCompact.mem_nhdsSet_inf_of_forall, map_nhdsSet_induced_eq, IsCompact.exists_thickening_image_subset, IsOpenMap.map_nhdsSet_eq, IsOpen.mem_nhdsSet_self, nhdsSetWithin_univ, Icc_mem_nhdsSet_Ico, Ioi_mem_nhdsSet_Ioc, Ico_mem_nhdsSet_Ioc, isClosedMap_iff_comap_nhds_le, nhdsSet_diagonal_eq_uniformity, nhdsSet_le, nhdsSet_empty, nhdsSet_iUnion, Set.ordT5Nhd_mem_nhdsSet, Ioi_mem_nhdsSet_Ico, hasBasis_nhdsSet_Ici_Ioi, Ioc_mem_nhdsSet_Ico, eventually_nhdsSet_iUnion₂, Ioo_mem_nhdsSet_Icc, Metric.disjoint_cobounded_nhdsSet, Ioc_mem_nhdsSet_Icc, nhdsSet_mono, Filter.eventually_nhdsSet_prod_iff, Ioi_mem_nhdsSet_Ici, IsCompact.mem_nhdsSet_prod_of_forall, nhdsKer_eq_nhdsKer_iff_nhdsSet, Iio_mem_nhdsSet_Iic, SeparatedNhds.disjoint_nhdsSet, Iic_mem_nhdsSet_Icc, disjoint_nhdsSet_principal, Iio_mem_nhdsSet_Iic_iff, IsCompact.mem_inf_nhdsSet_of_forall, lift'_nhdsSet_interior, Icc_mem_nhdsSet_Icc, exists_contMDiffMap_zero_one_nhds_of_isClosed, nhdsSet_iInter_le, hasBasis_nhdsSet, nhds_prod_le_of_disjoint_cocompact, mem_nhdsSet_iff_exists, IsLindelof.disjoint_nhdsSet_left, IsClosedMap.comap_nhdsSet_eq, hasBasis_nhdsSet_Iic_Iic, eventually_nhdsSet_iff_exists, Continuous.tendsto_nhdsSet, nhdsSet_sInter_le, IsCompact.disjoint_nhdsSet_left, IsClosedMap.comap_nhds_le, IsLindelof.disjoint_nhdsSet_right, Ioo_mem_nhdsSet_Ioc, Icc_mem_nhdsSet_Ioc, Ico_mem_nhdsSet_Ico, nhdsSet_basis_nhdsKer, nhdsSet_le_iff, separatedNhds_iff_disjoint, disjoint_nhdsSet_nhdsSet, nhdsSet_eq_bot_iff, nhdsSet_diagonal_le_uniformity, bUnion_mem_nhdsSet, eventually_nhdsSet_iUnion, mem_nhdsSet_iff_forall, isClosedMap_iff_comap_nhdsSet_le, exists_mem_nhdsSet_isCompact_mapsTo, nhdsSet_inj_iff, Iio_mem_nhdsSet_Icc, hasBasis_nhdsSet_Iic_Iio, injective_nhdsSet, Ico_mem_nhdsSet_Icc, Iio_mem_nhdsSet_Ico, IsCompact.nhdsSet_prod_eq, Metric.hasBasis_nhdsSet_cthickening, IsCompact.prod_nhdsSet_eq_biSup, CompletelyNormalSpace.completely_normal, compl_singleton_mem_nhdsSet_iff, Ici_mem_nhdsSet_Icc, forall_restrictGermPredicate_iff, nhdsSet_Iic, RegularSpace.regular, Topology.IsUpperSet.nhdsSet_eq_principal_upperClosure, nhdsSet_eq_principal_iff, Metric.cthickening_mem_nhdsSet, nhdsSet_prod_le_of_disjoint_cocompact, nhdsSet_Ici, IsCompact.elim_nhds_subcover_nhdsSet, upperHemicontinuousWithinAt_iff, Set.InjOn.exists_mem_nhdsSet, nhdsSet_neBot_iff, disjoint_nhds_nhdsSet, nhdsSet_Iio, IsCompact.nhdsSet_prod_eq_biSup, subset_interior_iff_mem_nhdsSet, nhdsSet_univ, nhdsSet_Ioc, nhdsSet_Icc, nhdsSet_prod_le, Ici_mem_nhdsSet_Ioc, Topology.IsInducing.nhdsSet_eq_comap, Filter.Eventually.union_nhdsSet, Iic_mem_nhdsSet_Ioc, Ici_mem_nhdsSet_Ico, Topology.IsInducing.map_nhdsSet_eq, IsClosed.nhdsSet_le_sup, IsClosed.nhdsSet_le_sup', Metric.hasBasis_nhdsSet_thickening, IsCompact.inf_nhdsSet_eq_biSup, IsCompact.mem_prod_nhdsSet_of_forall, nhdsSet_diagonal, Ici_mem_nhdsSet_Ici, IsCompact.nhdsSet_inter_eq, disjoint_principal_nhdsSet, regularSpace_generateFrom, upperHemicontinuousAt_iff, IsCompact.nhdsSet_basis_isCompact_isClosed, regularSpace_iff, Iic_mem_nhdsSet_Iic_iff, Iio_mem_nhdsSet_Ioc, Ioi_mem_nhdsSet_Ici_iff, hasBasis_nhdsSet_Ici_Ici, Ioc_mem_nhdsSet_Ioc, monotone_nhdsSet, SeparationQuotient.comap_mk_nhdsSet_image, SeparationQuotient.comap_mk_nhdsSet, IsCompact.lift'_closure_nhdsSet, mem_nhdsSet_induced, nhdsSet_inter_le, principal_nhdsKer, nhdsSet_induced, nhdsKer_mem_nhdsSet, IsCompact.nhdsSet_inf_eq_biSup, Iic_mem_nhdsSet_Ico, IsCompact.elim_nhds_subcover_nhdsSet', mem_nhdsSet_interior, prod_nhdsSet_le_of_disjoint_cocompact, Metric.thickening_mem_nhdsSet, Ici_mem_nhdsSet_Ici_iff, nhdsSet_interior, IsCompact.disjoint_nhdsSet_right, Topology.IsLowerSet.nhdsSet_eq_principal_lowerClosure, IsOpen.nhdsSet_eq, nhdsSet_singleton, Metric.disjoint_nhdsSet_cobounded, disjoint_nhdsSet_nhds, exists_smooth_zero_one_nhds_of_isClosed, IsCompact.nhdsSet_basis_uniformity, Iic_mem_nhdsSet_Iic, nhdsSet_Ico, Ioi_mem_nhdsSet_Icc, IsCompact.disjoint_nhdsSet_nhds, eventually_nhdsSet_iff_forall, Ioo_mem_nhdsSet_Ico, mem_nhdsSet, exists_contMDiffMap_one_nhds_of_subset_interior, nhdsSet_Ioi, nhdsSet_nhdsKer, IsOpen.mem_nhdsSet, IsClosedMap.comap_nhdsSet_le, IsCompact.nhdsSet_basis_isCompact, principal_le_nhdsSet, nhds_le_nhdsSet_iff, map_nhdsSet_subtype_val
nhdsSetWithin 📖	CompOp	20 math math: mem_nhdsSet_subtype_iff_nhdsSetWithin, map_nhdsSet_induced_eq, nhdsSetWithin_hasBasis, nhdsSetWithin_univ, nhdsSetWithin_univ', IsCompact.nhdsSetWithin_prod_eq, nhdsSetWithin_basis_open, nhdsSetWithin_eq_principal_of_subset, nhdsSetWithin_mono_right, nhdsSetWithin_self, ContinuousOn.preimage_mem_nhdsSetWithin_of_mem_nhdsSet, nhdsSetWithin_empty', principal_inter_le_nhdsSetWithin, Topology.IsInducing.map_nhdsSet_eq, nhdsSetWithin_empty, nhdsSetWithin_mono_left, mem_nhdsSetWithin, nhdsSetWithin_singleton, nhdsSetWithin_prod_le, map_nhdsSet_subtype_val
nhdsWithin 📖	CompOp	829 math math: Metric.nhdsWithin_basis_eball, PredOrder.nhdsGT_eq_nhdsNE, absorbent_iff_eventually_nhdsNE_zero, Ioc_mem_nhdsLE, Topology.IsInducing.map_nhdsWithin_eq, hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt, tendsto_zero_iff_meromorphicOrderAt_pos, OpenPartialHomeomorph.map_extend_nhdsWithin_eq_image, map_nhdsWithin, Function.LeftInverse.map_nhds_eq, IsOpen.nhdsWithin_eq, Filter.map_add_right_nhdsGT, nhdsWithin_insert, Complex.tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero, nhdsWithin_Ioi_neBot', Ico_mem_nhdsLT, eventually_nhds_nhdsWithin, nhdsWithin_singleton, HasDerivWithinAt.liminf_right_slope_norm_le, Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le, tendsto_norm_sub_self_nhdsNE, Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE, nhds_ne_subtype_neBot_iff, Convex.nhdsWithin_diff_eq_nhdsNE, inv_atBot₀, tendsto_ceil_right', nhdsWithin_Ici_isMeasurablyGenerated, OpenPartialHomeomorph.eventually_ne_nhdsWithin, nhdsWithin_le_comap, Set.OrdConnected.mem_nhdsLT, Metric.continuousWithinAt_iff', punctured_nhds_smul, HasDerivWithinAt.liminf_right_slope_le, OnePoint.nhdsWithin_coe, OnePoint.nhdsWithin_coe_image, nhds_ne_subtype_eq_bot_iff, CFC.tendsto_cfc_rpow_sub_one_log, tendsto_cobounded_iff_meromorphicOrderAt_neg, HasDerivWithinAt.eventually_ne, mem_codiscreteWithin_iff_forall_mem_nhdsNE, comap_coe_Ioi_nhdsGT, eventually_mem_nhdsWithin_iff, tendsto_inv_nhdsLE, Filter.inv_nhdsWithin_ne_zero, HasFPowerSeriesAt.locally_ne_zero, Function.Periodic.tendsto_nhds_zero, tendsto_zpow_nhdsNE_zero_cobounded, nhdsWithin_biUnion, mapClusterPt_leftLim, nhdsWithin_uIoo_right_le_nhdsNE, Uniform.continuousOn_iff'_left, mem_nhdsLT_iff_exists_Ico_subset, contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin, AntitoneOn.tendsto_nhdsGT, Antitone.tendsto_rightLim, EMetric.nhdsWithin_basis_closed_eball, eventually_enorm_mfderivWithin_symm_extChartAt_lt, Set.EqOn.eventuallyEq_nhdsWithin, Function.Periodic.cuspFunction_zero_eq_limUnder_nhds_ne, OrderDual.instNeBotNhdsWithinIio, map_extChartAt_symm_nhdsWithin, nhdsWithin_Iio_self_neBot', exists_seq_strictMono_tendsto_nhdsWithin, nhdsWithin_Ioi_isMeasurablyGenerated, nhdsWithin_Iio_neBot, nhdsWithin_basis_open, mem_nhdsGT_iff_exists_mem_Ioc_Ioo_subset, Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet, MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdsNE, nhdsWithin_Ioo_eq_nhdsLT, Real.tendsto_cos_pi_div_two, inter_mem_nhdsWithin, HasDerivWithinAt.liminf_right_norm_slope_le, tendsto_norm_nhdsNE_one, one_mem_posTangentConeAt_iff_frequently, OpenPartialHomeomorph.map_extend_nhdsWithin_eq_image_of_subset, isDiscrete_iff_nhdsWithin, tendsto_inv_nhdsGE_inv, ContDiffWithinAt.eventually, instNeBotNhdsWithinComplSetSingletonOfNontrivial, inv_atTop₀, hasDerivWithinAt_iff_isLittleO, LowerSemicontinuousOn.le_liminf, Real.tendsto_tsum_powerSeries_nhdsWithin_lt, Filter.map_mul_right_nhdsGT, tendsto_fract_left', HasFPowerSeriesWithinAt.eventually, HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt, map_extChartAt_symm_nhdsWithin', Function.update_eventuallyEq_nhdsNE, nhdsWithin_neBot_of_mem, OpenPartialHomeomorph.map_nhdsWithin_eq, IsCompact.mem_uniformity_of_prod, Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzCone, Real.punctured_nhds_module_neBot, nhdsWithin_uIcc_isMeasurablyGenerated, comap_coe_nhdsLT_of_Ioo_subset, OpenPartialHomeomorph.extend_target_mem_nhdsWithin, mem_nhdsGT_iff_exists_Ioc_subset, tendsto_nhdsWithin_iff, map_extChartAt_symm_nhdsWithin_range', MeromorphicAt.eq_nhdsNE_toMeromorphicNFAt, WeakFEPair.hf_zero', exists_nhds_ne_inf_principal_neBot, tendsto_floor_right_pure, MonotoneOn.tendsto_nhdsLT, Filter.inv_nhdsNE_zero, Icc_mem_nhdsGE, nhdsGT_basis_of_exists_gt, map_extChartAt_symm_nhdsWithin_range, comap_norm_nhdsGT_zero, HasDerivAt.eventually_ne, eventually_nhdsWithin_eventually_nhds_iff_of_isOpen, map_extChartAt_nhdsWithin', nhdsLT_neBot_of_exists_lt, nhdsWithin_Ico_eq_nhdsGE, eventually_mem_nhdsWithin, tendsto_norm_inv_nhdsNE_zero_atTop, dslope_eventuallyEq_slope_nhdsNE, nhdsWithin_sUnion, Absorbs.eventually_nhdsNE_zero, tendsto_inv_nhdsLE_inv, nhdsWithin_of_mem_discrete, comap_nhdsWithin_range, MeasureTheory.tendsto_measure_biInter_gt, nhdsWithin_univ, tendsto_inv_nhdsGT_inv, tendsto_inv_nhdsWithin_Iic_inv, equicontinuousWithinAt_iff_pair, EMetric.tendstoLocallyUniformlyOn_iff, indicator_thickening_eventually_eq_indicator_closure, tendsto_ceil_left_pure_ceil, contDiffWithinAt_nat, AnalyticAt.frequently_zero_iff_eventually_zero, HasFDerivWithinAt.eventually_notMem, HasLineDerivAt.tendsto_slope_zero_right, Filter.inv_nhdsGT, nhdsWithin_eq_nhdsWithin, meromorphicOrderAt_ne_top_iff, upperHemicontinuousWithinAt_iff_forall_isOpen, Asymptotics.isLittleO_insert, meromorphicOrderAt_eq_top_iff, CovBy.nhdsGE, IsLocalMinOn.not_nhds_le_map, nhdsNE_le_cofinite, Homeomorph.map_punctured_nhds_eq, OnePoint.nhdsNE_infty_neBot, preimage_coe_mem_nhds_subtype, nhdsWithin_Icc_eq_nhdsLE, SeparationQuotient.tendsto_lift₂_nhdsWithin, Convex.nhdsWithin_inter_Iio_eq_nhdsLT, taylor_tendsto, nhdsWithin_Iic_isMeasurablyGenerated, Prod.instNeBotNhdsWithinIio, EMetric.nhdsWithin_basis_eball, IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mul'', NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT, Module.punctured_nhds_neBot, Convex.nhdsWithin_diff_eq_nhdsLT, mem_nhdsWithin_self_inter, extChartAt_target_mem_nhdsWithin, tendsto_cobounded_of_meromorphicOrderAt_neg, eventually_norm_mfderivWithin_symm_extChartAt_lt, nhdsWithin_pi_univ_eq, nhdsWithin_eq_comap_uniformity_of_mem, SuccOrder.nhdsLE_eq_nhds, countable_setOf_isolated_right, AntitoneOn.tendsto_nhdsWithin_Ioo_right, accPt_principal_iff_nhdsWithin, Filter.inv_cobounded₀, map_coe_Ioo_atBot, nhdsLT_basis_of_exists_lt, tendsto_neg_nhdsGT_neg, Complex.differentiableOn_update_limUnder_of_bddAbove, nhdsWithin_eq_map_subtype_coe, contDiffWithinAt_iff_contDiffOn_nhds, tendsto_ceil_right_pure_add_one, HasDerivWithinAt.eventually_notMem, upperHemicontinuousWithinAt_iff_preimage_Iic, Set.OrdConnected.mem_nhdsGT, eventuallyEq_toIocDiv_nhdsGT, Filter.map_add_left_nhdsNE, PredOrder.nhdsGE_eq_nhds, Monotone.tendsto_nhdsLT, EReal.tendsto_toReal_atTop, mem_nhdsGT_iff_exists_Ioo_subset', Metric.mem_nhdsWithin_iff, tendsto_comp_coe_Iio_atTop, EReal.tendsto_toReal_atBot, map_fst_nhdsWithin, hasDerivAt_iff_tendsto_slope_left_right, tendsto_norm_div_self_nhdsNE, tendsto_floor_right_pure_floor, OpenPartialHomeomorph.extend_image_target_mem_nhds, intervalIntegral.FTCFilter.nhdsWithinSingleton, LowerSemicontinuousWithinAt.le_liminf, mem_codiscrete, tendsto_norm_div_self_nhdsGE, OpenPartialHomeomorph.eventually_nhdsWithin, tendsto_sub_mul_tsum_nat_cpow, Besicovitch.ae_tendsto_rnDeriv, HasProdLocallyUniformlyOn.exists_hasProdUniformlyOn, Function.Periodic.boundedAtFilter_cuspFunction, nhdsGT_basis, IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mul, Icc_mem_nhdsGT, Ico_mem_nhdsLT_of_mem, Metric.tendsto_nhdsWithin_nhds, contDiffWithinAt_zero, mem_nhdsLT_iff_exists_mem_Ico_Ioo_subset, tendsto_Ioi_atBot, nhdsWithinLE_sup_nhdsWithinGT, Prod.instNeBotNhdsWithinIoi, nhdsLE_eq_iInf_principal, absorbs_iff_eventually_nhdsNE_zero, tendsto_fract_right', Real.tendsto_cos_neg_pi_div_two, Set.LeftInvOn.map_nhdsWithin_eq, tendsto_riemannZeta_sub_one_div, eventually_ne_nhdsWithin, ZetaAsymptotics.tendsto_Gamma_term_aux, nhdsWithin_compl_singleton_le, extChartAt_target_mem_nhdsWithin_of_mem, nhdsWithin_eq_iff_eventuallyEq, Antitone.tendsto_nhdsGT, Topology.IsInducing.image_mem_nhdsWithin, Filter.HasBasis.equicontinuousWithinAt_iff_right, MeromorphicAt.tendsto_nhds_meromorphicTrailingCoeffAt, Set.MapsTo.preimage_mem_nhdsWithin, intervalIntegral.FTCFilter.nhdsUIcc, StrongFEPair.hf_zero', isClosed_and_discrete_iff, contDiffWithinAt_iff_of_ne_infty, tendsto_inv_nhdsGT_zero, nhdsWithin_eq_nhds, ModelWithCorners.map_nhdsWithin_eq, HasLineDerivAt.tendsto_slope_zero, Complex.tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero, Real.tendsto_sin_neg_pi_div_two, Filter.map_add_right_nhdsNE, mem_nhdsWithin_iff_eventuallyEq, Uniform.continuousWithinAt_iff'_right, HasFTaylorSeriesUpToOn.exists_lipschitzOnWith_of_nnnorm_lt, nhdsGE_eq_iInf_principal, NNReal.map_coe_nhdsGT, frequently_nhds_subtype_iff, Filter.inv_nhdsNE, MonotoneOn.tendsto_nhdsGT, MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre, nhdsLE_basis_of_exists_lt, tendsto_neg_nhdsLT_neg, IsUnifLocDoublingMeasure.exists_measure_closedBall_le_mul', ContDiffWithinAt.restrictScalars_iteratedFDerivWithin_eventuallyEq, Complex.comap_exp_nhdsNE, upperHemicontinuousOn_iff_preimage_Iic, mem_closure_ne_iff_frequently_within, mapClusterPt_rightLim, OpenPartialHomeomorph.map_extend_symm_nhdsWithin, nhdsWithin_eq_comap_uniformity, Complex.nhdsWithin_lt_le_nhdsWithin_stolzSet, HurwitzZeta.completedHurwitzZetaEven_residue_one, upperSemicontinuousWithinAt_iff_limsup_le, AnalyticWithinAt.eventually_analyticWithinAt, tendsto_ceil_right_pure_floor_add_one, codiscreteWithin_iff_locallyEmptyComplementWithin, Convex.taylor_approx_two_segment, UpperSemicontinuousWithinAt.limsup_le, nhds_eq_nhdsWithin_sup_nhdsWithin, tendsto_ceil_left, Set.OrdConnected.mem_nhdsGE, HasLineDerivAt.tendsto_slope_zero_left, tendsto_nhds_iff_meromorphicOrderAt_nonneg, intervalIntegral.FTCFilter.nhdsIcc, IsTopologicalAddGroup.tendstoLocallyUniformlyOn_iff, UpperHemicontinuousWithinAt.forall_isOpen, comap_norm_nhdsGT_zero', tendsto_nhdsWithin_range, upperSemicontinuousOn_iff_limsup_le, ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ, Complex.tendsto_norm_tan_atTop, ContinuousWithinAt.tendsto_nhdsWithin, map_snd_nhdsWithin, Complex.tendsto_self_mul_Gamma_nhds_zero, tendsto_inv_atBot_nhdsLT_zero, Filter.neg_nhdsGT, OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin', OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin, HasDerivAt.tendsto_slope_zero_left, IsLocalExtrOn.not_nhds_le_map, Filter.inv_nhdsLT, Complex.tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero, NormedField.nhdsNE_neBot, Complex.map_exp_comap_re_atBot, HasDerivAt.tendsto_nhdsNE, Filter.map_add_left_nhdsLT, Ioo_mem_nhdsLT_of_mem, Uniform.continuousOn_iff'_right, inv_nhdsGT_zero, tendsto_abs_nhdsNE_zero, insert_mem_nhdsWithin_of_subset_insert, nhdsWithin_Icc_eq_nhdsGE, Ioc_mem_nhdsGT, deriv.lhopital_zero_nhds, MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt, Icc_mem_nhdsGE_of_mem, Ico_mem_nhdsLE_of_mem, meromorphicOrderAt_eq_int_iff, Ioc_mem_nhdsLT, intervalIntegral.FTCFilter.nhdsRight, MeasureTheory.Filtration.rightCont_apply, tendsto_measure_thickening, LocallyFinite.nhdsWithin_iUnion, ContDiffWithinAt.contDiffOn, tendsto_rpow_sub_one_log, MeromorphicAt.eventuallyEq_zero_nhdsNE_of_eventuallyEq_zero_codiscreteWithin, Convex.isLittleO_alternate_sum_square, Uniform.continuousWithinAt_iff'_left, nhdsLE_eq_iInf_inf_principal, tendsto_inv_atTop_nhdsGT_zero, tendsto_zero_of_meromorphicOrderAt_pos, Ne.nhdsWithin_diff_singleton, OpenPartialHomeomorph.nhdsWithin_target_inter, HasDerivWithinAt.limsup_norm_slope_le, CovBy.nhdsGT, Metric.tendsto_nhdsWithin_nhdsWithin, accPt_iff_frequently_nhdsNE, isLittleO_log_rpow_nhdsGT_zero, comap_mulLeft_nhdsGT_zero, IsLUB.nhdsWithin_neBot, Real.tendsto_comp_exp_atBot, nhdsLT_sup_nhdsGE, OpenPartialHomeomorph.map_extend_nhds, ModelWithCorners.symm_map_nhdsWithin_range, extChartAt_target_mem_nhdsWithin', IsUnifLocDoublingMeasure.eventually_measure_le_doublingConstant_mul, tendsto_floor_right, intervalIntegral.FTCFilter.nhdsUniv, lim_nhdsWithin, Ne.nhdsWithin_compl_singleton, mem_nhdsWithin_iff_eventually, ENNReal.nhdsGT_zero_neBot, Ico_mem_nhdsGT_of_mem, mem_nhdsWithin, eventually_nhdsWithin_of_eventually_nhds, Absorbent.eventually_nhdsNE_zero, MeasureTheory.Filtration.rightCont_def, MeromorphicAt.eventually_continuousAt, HurwitzZeta.hurwitzZeta_residue_one, Antitone.tendsto_leftLim, mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset, OpenPartialHomeomorph.map_nhdsWithin_preimage_eq, UpperHemicontinuousOn.forall_isOpen, HasDerivWithinAt.limsup_slope_norm_le, DifferentiableWithinAt.isBigOTVS_sub, tendsto_measure_Icc_nhdsWithin_right, mem_closure_iff_nhdsWithin_neBot, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contDiffOn_succ_iff_hasFDerivWithinAt, tendsto_integral_mulExpNegMulSq_comp, exists_nhds_ne_neBot, UpperSemicontinuousOn.limsup_le, continuousOn_update_iff, tendsto_ne_zero_of_meromorphicOrderAt_eq_zero, contMDiffWithinAt_iff_contMDiffOn_nhds, Filter.map_mul_left_nhdsLT, HasFDerivWithinAt.isBigO_sub, Real.tendsto_log_nhdsGT_zero, ContDiffWithinAt.eventually_hasFTaylorSeriesUpToOn, isLittleO_abs_log_rpow_rpow_nhdsGT_zero, mem_nhdsWithin_of_mem_nhds, Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE, ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range, Filter.neg_nhdsLT, nhdsWithin_eq_nhdsWithin', Asymptotics.isBigOWith_insert, Tactic.ComputeAsymptotics.tendsto_nhdsGT_of_tendsto_atTop, ENNReal.nhdsGT_coe_neBot, nhdsGT_le_nhdsNE, HurwitzZeta.completedCosZeta_residue_zero, Real.tendsto_log_nhdsLT_zero, tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero, tangentConeAt_def, IsGLB.frequently_mem, ModelWithCorners.map_nhds_eq, HasFDerivAt.eventually_notMem, ContinuousWithinAt.preimage_mem_nhdsWithin, Ioo_mem_nhdsLT, HasFPowerSeriesAt.eventually, Filter.tendsto_inv₀_nhdsWithin_ne_zero, nhdsWithin_eq, HasFDerivWithinAt.tendsto_nhdsWithin_nhdsNE, eventuallyEq_toIcoDiv_nhdsLT, MeasureTheory.mul_le_addHaar_image_of_lt_det, nhdsWithin_subtype, hasDerivAt_iff_tendsto_slope_zero, nhdsWithin_Iio_isMeasurablyGenerated, comap_coe_nhdsLT_eq_atTop_iff, upperHemicontinuousOn_iff_forall_isOpen, WeakFEPair.hf_zero, MeromorphicAt.eventually_analyticAt, TFAE_mem_nhdsGT, nhdsWithin_restrict', tendsto_ceil_left_pure, Real.taylor_tendsto, tendsto_log_div_rpow_nhdsGT_zero, Real.tendsto_logb_nhdsNE_zero_of_base_lt_one, ModelWithCorners.image_mem_nhdsWithin, tendsto_floor_left', Besicovitch.ae_tendsto_measure_inter_div, MeasureTheory.integrableOn_Ioi_iff_integrableAtFilter_atTop_nhdsWithin, mem_nhdsWithin_inter_self, map_coe_Ioo_atTop, NormedField.tendsto_norm_inv_nhdsNE_zero_atTop, MonotoneOn.tendsto_nhdsWithin_Ioo_right, Ioo_mem_nhdsLE_of_mem, map_coe_atBot_of_Ioo_subset, IsDenseInducing.nhdsWithin_neBot, ConnectedSpace.neBot_nhdsWithin_compl_of_nontrivial_of_t1space, tendsto_neg_nhdsLE_neg, map_extChartAt_nhds', map_coe_Ioi_atBot, tendsto_rpow_neg_nhdsGT_zero, MonotoneOn.tendsto_nhdsWithin_Ioo_left, eventuallyEq_nhdsWithin_iff, Filter.neg_nhdsNE, ContinuousOn.integrableAt_nhdsWithin, HasFTaylorSeriesUpToOn.exists_lipschitzOnWith, tendsto_neg_nhdsGE, tendsto_gauge_nhds_zero_nhdsGE, tendsto_nhdsLT_zero_of_comp_inv_tendsto_atBot, IsDiscrete.nhdsWithin, pure_le_nhdsWithin, Tactic.ComputeAsymptotics.tendsto_nhdsLT_of_tendsto_atTop, ContDiffWithinAt.laplacianWithin_CLM_comp_left_nhds, DenseRange.nhdsWithin_neBot, nhdsWithinLT_sup_nhdsWithinGT, eventually_nhdsNE_eventually_nhds_iff, Real.tendsto_abs_tan_of_cos_eq_zero, mem_nhdsLT_iff_exists_Ioo_subset', Antitone.tendsto_rightLim_within, Topology.IsOpenEmbedding.map_nhdsWithin_preimage_eq, LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg, Metric.nhdsWithin_basis_closedEBall, nhdsLT_basis, nhdsWithin_pi_neBot, Real.tendsto_tan_pi_div_two, VectorField.eventuallyEq_mpullback_mpullbackWithin_extChartAt, upperHemicontinuousWithinAt_iff, IsGLB.nhdsWithin_neBot, MeasureTheory.integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin, map_extChartAt_nhdsWithin, right_nhdsWithin_Ioo_neBot, tendsto_nhdsWithin_iff_subtype, MeasureTheory.addHaar_image_le_mul_of_det_lt, tendsto_comp_coe_Ioo_atBot, nhdsWithin_le_nhds, ContinuousWithinAt.tendsto_nhdsWithin_image, Tactic.ComputeAsymptotics.tendsto_nhdsNE_of_tendsto_atTop, continuousAt_iff_punctured_nhds, HasDerivAt.lhopital_zero_nhds, MeromorphicAt.frequently_eq_iff_eventuallyEq, Ioc_mem_nhdsGT_of_mem, inv_nhdsLT_zero, SuccOrder.nhdsGT, mem_nhdsWithin_insert, HasDerivAt.tendsto_slope, nhdsGE_basis_Icc, Ioc_mem_nhdsLT_of_mem, Antitone.tendsto_leftLim_within, taylor_isLittleO, MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero, tendsto_nhdsWithin_of_tendsto_nhds, RightDerivMeasurableAux.A_mem_nhdsGT, Filter.map_add_right_nhdsLT, lowerSemicontinuousWithinAt_iff, Complex.tendsto_norm_tan_of_cos_eq_zero, PredOrder.nhdsLT, TFAE_mem_nhdsGE, lowerSemicontinuousWithinAt_iff_le_liminf, ModelWithCorners.symm_map_nhdsWithin_image, Real.tendstoLocallyUniformlyOn_rpow_sub_one_log, Function.Periodic.invQParam_tendsto, Filter.map_mul_left_nhdsGT, mem_codiscreteWithin, self_mem_nhdsWithin, eventuallyEq_toIcoDiv_nhdsGE, isDiscrete_iff_nhdsNE, tendsto_neg_nhdsGE_neg, mem_nhdsGE_iff_exists_Ico_subset, left_nhdsWithin_Ioo_neBot, Real.map_exp_atBot, nhdsLT_le_nhdsNE, mem_nhdsWithin_prod_iff, left_nhdsWithin_Ioc_neBot, tendsto_neg_nhdsGT, mem_nhdsLT_iff_exists_Ioo_subset, Filter.map_mul_right_nhdsLT, nhdsWithin_extChartAt_target_eq_of_mem, HasDerivWithinAt.limsup_slope_le', OnePoint.nhdsNE_infty_eq, HasFPowerSeriesWithinAt.isBigO_sub_partialSum_pow, Metric.tendstoLocallyUniformlyOn_iff, HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub, mem_nhds_subtype_iff_nhdsWithin, nhdsWithin_Ioc_eq_nhdsGT, OpenPartialHomeomorph.eventually_nhdsWithin', Ico_mem_nhdsGE_of_mem, MeromorphicOn.eventually_analyticAt_or_mem_compl, tendsto_ceil_left', AntitoneOn.tendsto_nhdsLT, nhdsWithin_pi_eq, MeasureTheory.Measure.mem_support_restrict, extChartAt_source_mem_nhdsWithin, nhdsWithin_uIoo_left_le_nhdsNE, nhdsWithin_empty, AnalyticWithinAt.exists_mem_nhdsWithin_analyticOn, hasLineDerivAt_iff_tendsto_slope_zero, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, HasFDerivWithinAt.eventually_ne, Real.tendsto_tan_neg_pi_div_two, isOpen_setOf_eventually_nhdsWithin, notMem_closure_iff_nhdsWithin_eq_bot, Antitone.tendsto_nhdsLT, MeromorphicNFAt.eventuallyEq_nhdsNE_iff_eventuallyEq_nhds, tendsto_fract_left, writtenInExtChartAt_sumSwap_eventuallyEq_id, IsUnifLocDoublingMeasure.eventually_measure_le_scaling_constant_mul', Function.Periodic.qParam_tendsto, Complex.Gammaℝ_residue_zero, eventually_nhdsWithin_iff, Topology.IsEmbedding.map_nhdsWithin_eq, IsTopologicalGroup.tendstoLocallyUniformlyOn_iff, mem_nhdsLE_iff_exists_Ioc_subset', mem_nhdsGE_iff_exists_Ico_subset', Real.tendsto_arctan_atTop, nhdsWithin_Ioc_eq_nhdsLE, nhdsWithin_inter, punctured_nhds_eq_nhdsWithin_sup_nhdsWithin, Function.Periodic.eventually_differentiableAt_cuspFunction_nhds_ne_zero, HasDerivAt.eventually_notMem, HasDerivWithinAt.tendsto_nhdsWithin_nhdsNE, eventually_nhds_subtype_iff, discreteTopology_subtype_iff, ContDiffAt.laplacianWithin_add_nhdsWithin, nhdsWithin_subtype_eq_bot_iff, ENNReal.nhdsLT_neBot, nhdsWithin_le_iff, Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le_of_imp, Real.comap_exp_nhdsGT_zero, Monotone.tendsto_rightLim, Monotone.tendsto_leftLim_within, OpenPartialHomeomorph.map_extend_nhdsWithin, tendsto_comp_coe_Ioo_atTop, EMetric.tendsto_nhdsWithin_nhds, tendsto_inv_nhdsGE, AnalyticAt.eventually_eq_or_eventually_ne, nhds_subtype_eq_comap_nhdsWithin, NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop, tendsto_inv_nhdsLT_zero, AnalyticAt.eventually_eq_zero_or_eventually_ne_zero, eventuallyConst_nhdsNE_iff_meromorphicOrderAt_sub_eq_top, nhdsWithinLE_sup_nhdsWithinGE, nhdsWithin_union, extChartAt_source_mem_nhdsWithin', nhdsGE_basis_of_exists_gt, ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin, isOpen_singleton_iff_punctured_nhds, Real.tendsto_arctan_atBot, OrderDual.instNeBotNhdsWithinIoi, tendsto_mulIndicator_thickening_mulIndicator_closure, OpenPartialHomeomorph.nhdsWithin_extend_target_eq, nhdsWithin_extChartAt_target_eq, tendsto_Ioo_atBot, nhdsWithin_prod_eq, tendsto_sub_mul_tsum_nat_rpow, Filter.map_mul_right_nhdsNE, nhdsWithin_pi_eq_bot, right_nhdsWithin_Ico_neBot, mem_nhdsLE_iff_exists_Icc_subset, eventually_eventually_nhdsWithin, nhdsWithin_restrict, nhdsLT_eq_bot_iff, nhdsLE_neBot, punctured_nhds_smul₀, tendsto_neg_nhdsLE, Icc_mem_nhdsGT_of_mem, map_extChartAt_nhdsWithin_eq_image', countable_setOf_isolated_left_within, upperSemicontinuousWithinAt_iff, MeasureTheory.Measure.finiteAt_nhdsWithin, MeasurableSet.nhdsWithin_isMeasurablyGenerated, ENNReal.nhdsGT_ofNat_neBot, analyticWithinAt_iff_exists_analyticAt, nhdsLE_basis_Icc, tendsto_floor_left_pure_ceil_sub_one, tendsto_inv_nhdsLT_inv, diff_mem_nhdsWithin_compl, PredOrder.nhdsLE, OpenPartialHomeomorph.nhdsWithin_source_inter, Real.tendsto_Icc_vitaliFamily_left, tendsto_measure_Icc_nhdsWithin_right', Complex.HadamardThreeLines.eventuallyle, InnerProductSpace.laplacianWithin_smul_nhds, TFAE_mem_nhdsLE, nhdsGT_eq_bot_iff, map_extChartAt_nhdsWithin_eq_image, nhdsGT_neBot_of_exists_gt, Ioc_mem_nhdsGE_of_mem, Tactic.ComputeAsymptotics.tendsto_nhdsNE_of_tendsto_atTop_nhds_of_eq, DifferentiableWithinAt.isBigO_sub, SuccOrder.nhdsGE, OnePoint.nhdsNE_coe_neBot, CovBy.nhdsLT, HasFDerivWithinAt.isBigOTVS_sub, HasDerivAt.tendsto_slope_zero, ENNReal.nhdsGT_nat_neBot, OpenPartialHomeomorph.IsImage.map_nhdsWithin_eq, eventuallyEq_toIocDiv_nhdsLE, nhdsLE_sup_nhdsGT, Besicovitch.tendsto_filterAt, Complex.nhdsWithin_stolzCone_le_nhdsWithin_stolzSet, Real.tendsto_logb_nhdsGT_zero_of_base_lt_one, Convex.diff_singleton_eventually_mem_nhds, Ioc_mem_nhdsLE_of_mem, IsLocalMaxOn.not_nhds_le_map, Ico_mem_nhdsGT, EMetric.tendsto_nhdsWithin_nhdsWithin, SeparationQuotient.tendsto_lift_nhdsWithin_mk, nhdsWithin_hasBasis, Real.tendsto_abs_tan_atTop, tendsto_norm_nhdsNE_zero, tendsto_const_nhdsWithin, perfectSpace_iff_forall_not_isolated, SeparationQuotient.map_mk_nhdsWithin_preimage, nhdsWithin_Iio_neBot', tendsto_Ioo_atTop, DirichletCharacter.LFunctionTrivChar_isBigO_near_one_horizontal, Icc_mem_nhdsLT, exists_seq_strictAnti_tendsto_nhdsWithin, DirichletCharacter.LFunctionTrivChar_residue_one, nhdsWithin_Iic_neBot, pure_sup_nhdsNE, ContinuousOn.integrableAt_nhdsWithin_of_isSeparable, mem_nhdsGT_iff_exists_Ioo_subset, completedRiemannZeta_residue_one, Asymptotics.IsBigO.id_rpow_of_le_one, TFAE_mem_nhdsLT, nhdsWithinLT_sup_nhdsWithinGE, MeromorphicAt.eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin, OpenPartialHomeomorph.extend_source_mem_nhdsWithin, nhdsGE_basis, LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul, tendsto_floor_left, intervalIntegral.FTCFilter.nhdsLeft, insert_mem_nhds_iff, HasFDerivAt.tendsto_nhdsNE, tendsto_ceil_right, tendsto_neg_nhdsLT, IsUnifLocDoublingMeasure.eventually_measure_le_scaling_constant_mul, Metric.continuousOn_iff', comap_coe_Iio_nhdsLT, frequently_nhdsWithin_iff, ZMod.LFunction_residue_one, UniformContinuousOn.tendstoUniformlyOn, map_nhds_induced_eq, hasGradientWithinAt_iff_tendsto, nhdsWithin_Ico_eq_nhdsLT, Complex.tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero, Filter.map_mul_left_nhdsNE, comap_coe_nhdsGT_of_Ioo_subset, Real.tendsto_sin_pi_div_two, tendstoLocallyUniformlyOn_iff_filter, TopologicalSpace.isCountablyGenerated_nhdsWithin, riemannZeta_residue_one, Ioo_mem_nhdsGE_of_mem, bsupr_limsup_dimH, continuousWithinAt_update_same, nhdsWithin_insert_of_ne, HurwitzZeta.completedHurwitzZetaEven_residue_zero, disjoint_nhdsWithin_of_mem_discrete, hasGradientWithinAt_iff_isLittleO, OpenPartialHomeomorph.map_extend_symm_nhdsWithin_range, nhdsWithin_pi_eq', ContMDiffWithinAt.contMDiffOn, nhdsLE_sup_nhdsGE, discreteTopology_iff_nhds_ne, tendsto_inv_nhdsLT, Ioo_mem_nhdsGT_of_mem, ContDiffWithinAt.analyticOn, Filter.tendsto_inv₀_nhdsNE_zero, ContinuousWithinAt.tendsto, IsUnifLocDoublingMeasure.exists_eventually_forall_measure_closedBall_le_mul, ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE, RightDerivMeasurableAux.B_mem_nhdsGT, nhdsWithin_Ioi_neBot, countable_setOf_isolated_left, Ico_mem_nhdsGE, DirichletCharacter.LFunction_isBigO_horizontal, Real.tendsto_log_nhdsNE_zero, Monotone.tendsto_rightLim_within, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, PartitionOfUnity.exists_finset_nhds', continuousOn_to_generateFrom_iff, hasDerivAt_iff_tendsto_slope, nhdsGT_sup_nhdsWithin_singleton, mulIndicator_thickening_eventually_eq_mulIndicator_closure, tendsto_fract_right, tendsto_floor_left_pure_sub_one, ImplicitFunctionData.map_implicitFunction_nhdsWithin_preimage, SmoothBumpFunction.nhdsWithin_range_basis, AnalyticAt.map_nhdsNE, nhdsWithin_Ioo_eq_nhdsGT, Set.OrdConnected.mem_nhdsLE, Metric.nhdsWithin_basis_ball, LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul', nhdsLT_sup_nhdsGT, nhds_bind_nhdsWithin, Convex.nhdsWithin_diff_eq_nhdsGT, nhdsLT_neBot, AnalyticAt.frequently_eq_iff_eventually_eq, Icc_mem_nhdsLE, hasFDerivWithinAt_iff_tendsto, tendsto_log_mul_rpow_nhdsGT_zero, EReal.nhdsWithin_top, tendsto_floor_right', limUnder_nhdsWithin_id, Asymptotics.isLittleOTVS_insert, hasDerivWithinAt_iff_tendsto_slope', preimage_nhdsWithin_coinduced', writtenInExtChartAt_sumInr_eventuallyEq_id, punctured_nhds_vadd, map_coe_atTop_of_Ioo_subset, tendsto_measure_thickening_of_isClosed, Convex.nhdsWithin_inter_Ioi_eq_nhdsGT, comap_coe_nhdsGT_eq_atBot_iff, Real.tendsto_logb_nhdsGT_zero, nhdsGE_eq_iInf_inf_principal, exists_continuousLinearEquiv_fderivWithin_symm_eq, EMetric.mem_nhdsWithin_iff, SuccOrder.nhdsLT_eq_nhdsNE, nhdsSetWithin_singleton, MeromorphicOn.eventually_analyticAt, Icc_mem_nhdsLT_of_mem, nhdsGT_neBot, tendsto_nhds_of_meromorphicOrderAt_nonneg, hasDerivWithinAt_iff_tendsto_slope, mem_nhdsWithin_subtype, mem_nhdsWithin_iff_exists_mem_nhds_inter, WeakFEPair.Λ_residue_zero, Ioo_mem_nhdsGT, ContDiffWithinAt.exists_lipschitzOnWith, Topology.IsEmbedding.map_nhds_eq, nhdsWithin_Icc_isMeasurablyGenerated, Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzSet, NormedField.nhdsWithin_isUnit_neBot, tendsto_norm_sub_self_nhdsGE, Monotone.tendsto_nhdsGT, MeasureTheory.tendsto_integral_meas_thickening_le, MeromorphicAt.frequently_zero_iff_eventuallyEq_zero, tendsto_log_mul_self_nhdsLT_zero, tendsto_indicator_thickening_indicator_closure, meromorphicOrderAt_ne_top_iff_eventually_ne_zero, EReal.nhdsWithin_bot, WeakFEPair.Λ_residue_k, UniformSpace.ball_mem_nhdsWithin, Real.tendsto_exp_atBot_nhdsGT, writtenInExtChartAt_sumInl_eventuallyEq_id, tendstoLocallyUniformlyOn_iff_forall_tendsto, lowerSemicontinuousOn_iff_le_liminf, Monotone.tendsto_leftLim, ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_nhds_right, singleton_mem_nhdsWithin_of_mem_discrete, continuousAt_update_same, nhdsWithin_inter', Real.tendsto_logb_nhdsNE_zero, nhdsWithin_iUnion, writtenInExtChartAt_comp, nhdsWithin_mono, eventuallyEq_nhdsWithin_of_eqOn, Filter.map_add_left_nhdsGT, hasDerivWithinAt_iff_tendsto, iSup_limsup_dimH, HasFiniteFPowerSeriesAt.eventually, NNReal.map_coe_nhdsGE, nhdsLE_basis, map_extChartAt_nhds, nhdsGE_neBot, tendsto_nhdsGT_zero_of_comp_inv_tendsto_atTop, ENNReal.nhdsGT_one_neBot, tendsto_comp_coe_Ioi_atBot, nhdsWithin_neBot, countable_setOf_isolated_right_within, tendsto_mabs_nhdsNE_one, LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div, MultipliableLocallyUniformlyOn.exists_multipliableUniformlyOn, Filter.tendsto_inv₀_cobounded', nhdsNE_sup_pure, map_nhds_subtype_val, HasFDerivAt.eventually_ne, Complex.tendsto_tsum_powerSeries_nhdsWithin_lt, mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset, tendsto_inv_nhdsGT, IsLUB.frequently_mem, comap_coe_Ioo_nhdsGT, AntitoneOn.tendsto_nhdsWithin_Ioo_left, nhdsWithin_extChartAt_target_eq', tendstoIxxNhdsWithin, HasDerivAt.tendsto_slope_zero_right, lowerHemicontinuousWithinAt_iff, tendsto_pow_atTop_nhdsWithin_zero_of_lt_one, CovBy.nhdsLE, mem_nhdsLE_iff_exists_Ioc_subset, Icc_mem_nhdsLE_of_mem, contDiffWithinAt_succ_iff_hasFDerivWithinAt, HasDerivWithinAt.limsup_slope_le, Real.tendsto_Icc_vitaliFamily_right, map_coe_Iio_atTop, tendsto_Iio_atTop, PerfectSpace.not_isolated, Complex.tendsto_exp_comap_re_atBot_nhdsNE, nhdsGE_basis_Ico, AnalyticWithinAt.exists_hasFTaylorSeriesUpToOn, Asymptotics.isBigO_one_nhds_ne_iff, Topology.IsInducing.map_nhds_eq, eventually_nhdsWithin_of_forall, HurwitzZeta.hurwitzZetaEven_residue_one, mem_nhdsGE_iff_exists_Icc_subset, nhdsWithin_Ici_neBot, comap_coe_Ioo_nhdsLT
specializationPreorder 📖	CompOp	2 math math: Continuous.specialization_monotone, closure_singleton_eq_Iic
«term_⤳_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nhds_def 📖	mathematical	—	nhds iInf Filter Set Filter.instInfSet Set.instMembership setOf IsOpen Filter.principal	—	—

---

← Back to Index