WithTop

📁 Source: Mathlib/Topology/Order/WithTop.lean

Statistics

Metric	Count
Definitions instWithTopOfOrderTopology, WithTop, neTopHomeomorph, sumHomeomorph	4
Theorems instOrderTopologyWithTop, instSecondCountableTopologyWithTop, continuousOn_untopA, continuousOn_untopD, continuous_coe, continuous_untop, isEmbedding_coe, isOpenEmbedding_coe, nhds_coe, tendsto_coe_atTop, tendsto_nhds_top_iff, tendsto_untop, tendsto_untopA, tendsto_untopD	14
Total	18

TopologicalSpace

Definitions

Name	Category	Theorems
instWithTopOfOrderTopology 📖	CompOp	15 math math: WithTop.continuousOn_untopD, instSecondCountableTopologyWithTop, instOrderTopologyWithTop, WithTop.tendsto_untop, WithTop.instBorelSpace, WithTop.isOpenEmbedding_coe, WithTop.continuous_coe, WithTop.tendsto_untopA, WithTop.isEmbedding_coe, WithTop.tendsto_untopD, WithTop.tendsto_coe_atTop, WithTop.tendsto_nhds_top_iff, WithTop.continuousOn_untopA, WithTop.continuous_untop, WithTop.nhds_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instOrderTopologyWithTop 📖	mathematical	—	OrderTopology WithTop instWithTopOfOrderTopology WithTop.instPreorder	—	—
instSecondCountableTopologyWithTop 📖	mathematical	—	SecondCountableTopology WithTop instWithTopOfOrderTopology	—	isEmpty_or_nonempty Finite.toSecondCountableTopology instFiniteWithTop Finite.of_subsingleton IsEmpty.instSubsingleton exists_countable_generateFrom_Ioi_Iio SeparableSpace.exists_countable_dense SecondCountableTopology.to_separableSpace le_antisymm le_generateFrom_iff_subset_isOpen isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom OrderTopology.topology_eq_generate_intervals instOrderTopologyWithTop isOpen_generateFrom_of_mem Set.union_singleton IsMax.Ioi_eq isOpen_iff_forall_mem_open Set.eq_empty_or_nonempty WithTop.Ioi_coe Set.image_empty Set.instLawfulSingleton Dense.exists_mem_open isOpen_Ioi' Set.Ioi_subset_Ioi LT.lt.le IsTopologicalBasis.isOpen_iff IsOpen.inter Set.Finite.isOpen_biInter isOpen_Iio' Set.Countable.union Set.Countable.image

WithTop

Definitions

Name	Category	Theorems
neTopHomeomorph 📖	CompOp	—
sumHomeomorph 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_untopA 📖	mathematical	—	ContinuousOn WithTop TopologicalSpace.instWithTopOfOrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder untopA setOf Top.top top	—	continuousOn_untopD
continuousOn_untopD 📖	mathematical	—	ContinuousOn WithTop TopologicalSpace.instWithTopOfOrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder untopD setOf Top.top top	—	ContinuousAt.continuousWithinAt tendsto_untopD
continuous_coe 📖	mathematical	—	Continuous WithTop TopologicalSpace.instWithTopOfOrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder some	—	Topology.IsEmbedding.continuous isEmbedding_coe
continuous_untop 📖	mathematical	—	Continuous Set.Elem WithTop setOf Top.top top instTopologicalSpaceSubtype Set Set.instMembership TopologicalSpace.instWithTopOfOrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder untop	—	continuous_iff_continuousAt tendsto_untop
isEmbedding_coe 📖	mathematical	—	Topology.IsEmbedding WithTop TopologicalSpace.instWithTopOfOrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder some	—	StrictMono.isEmbedding_of_ordConnected TopologicalSpace.instOrderTopologyWithTop coe_strictMono range_coe Set.ordConnected_Iio
isOpenEmbedding_coe 📖	mathematical	—	Topology.IsOpenEmbedding WithTop TopologicalSpace.instWithTopOfOrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder some	—	isEmbedding_coe range_coe isOpen_Iio instClosedIciTopology OrderTopology.to_orderClosedTopology TopologicalSpace.instOrderTopologyWithTop
nhds_coe 📖	mathematical	—	nhds WithTop TopologicalSpace.instWithTopOfOrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder some Filter.map	—	Topology.IsOpenEmbedding.map_nhds_eq isOpenEmbedding_coe
tendsto_coe_atTop 📖	mathematical	—	Filter.Tendsto WithTop some Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder nhds TopologicalSpace.instWithTopOfOrderTopology Top.top top	—	isEmpty_or_nonempty nhds_discrete Finite.instDiscreteTopology T2Space.t1Space OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology TopologicalSpace.instOrderTopologyWithTop instFiniteWithTop Finite.of_subsingleton IsEmpty.instSubsingleton Unique.instSubsingleton tendsto_nhds_top_iff Filter.mp_mem Filter.HasBasis.mem_of_mem Filter.atTop_basis_Ioi SemilatticeSup.instIsDirectedOrder Filter.univ_mem'
tendsto_nhds_top_iff 📖	mathematical	—	Filter.Tendsto WithTop nhds TopologicalSpace.instWithTopOfOrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Top.top top Filter.Eventually Preorder.toLT instPreorder some	—	isEmpty_or_nonempty nhds_discrete Finite.instDiscreteTopology T2Space.t1Space OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology TopologicalSpace.instOrderTopologyWithTop instFiniteWithTop Finite.of_subsingleton IsEmpty.instSubsingleton Filter.Eventually.of_forall Unique.instSubsingleton Filter.HasBasis.tendsto_right_iff nhds_top_basis nontrivial Set.forall_mem_range range_coe
tendsto_untop 📖	mathematical	—	Filter.Tendsto Set.Elem WithTop setOf Top.top top untop Set Set.instMembership nhds instTopologicalSpaceSubtype TopologicalSpace.instWithTopOfOrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Filter.Tendsto.comp tendsto_untopA tendsto_subtype_rng Filter.tendsto_id
tendsto_untopA 📖	mathematical	—	Filter.Tendsto WithTop untopA nhds TopologicalSpace.instWithTopOfOrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	tendsto_untopD
tendsto_untopD 📖	mathematical	—	Filter.Tendsto WithTop untopD nhds TopologicalSpace.instWithTopOfOrderTopology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	CanLift.prf canLift nhds_coe Filter.tendsto_map'_iff Filter.tendsto_id

(root)

Definitions

Name	Category	Theorems
WithTop 📖	CompOp	1092 math, 6 bridge math: CategoryTheory.Triangulated.TStructure.eTruncLT_map_app_eTruncLTι_app, ValueDistribution.logCounting_zero, TangentBundle.continuousLinearMapAt_model_space, MeasureTheory.IsStoppingTime.measurableSet_inter_le_iff, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₃, WithBot.coe_toDualTopEquiv_eq, instContMDiffAddOfNatWithTopENatOfContinuousAdd, WithBot.ofDual_map, WithTop.map_ofDual, fun_meromorphicOrderAt_pow_id_sub_const, tendsto_zero_iff_meromorphicOrderAt_pos, Finset.coe_inf', WithBot.add_le_add_iff_right', instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold, WithTop.recTopCoe_top, WithTop.coe_max, WithTop.lt_def, WithTop.pred_eq_pred, instLieAddGroupOfNatWithTopENat, Field.Emb.Cardinal.equivLim_coherence, MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top, LatticeHom.withTopWithBot_apply, OneHom.withTopMap_apply, WithTop.instWellFoundedGT, HahnSeries.untop_orderTop_of_ne_zero, MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range, HahnSeries.orderTop_single_le, contDiffOn_nat_succ_iff_contDiffOn_one_iteratedDerivWithin, WithTop.prod_lt_top, WithBot.lt_ofDual_iff, Complex.meromorphicOrderAt_canonicalFactor, fun_meromorphicOrderAt_div, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_deg, MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq, AnalyticOn.exists_hasFTaylorSeriesUpToOn, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, WithBotTop.coe_strictMono, LeftInvariantDerivation.leibniz, smooth_barycentric_coord, WithTop.lt_untopD_iff, ValueDistribution.proximity_zero, ContDiffOn.rpow_const_of_le, WithTop.toDualBotEquiv_coe, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₁, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₂, WithTop.sub_eq_top_iff, instIsContMDiffRiemannianBundleOfNatWithTopENat_1, MeasureTheory.stoppedProcess_stoppedProcess, WithTop.coe_mono, WithTop.Ico_coe_coe, Function.Embedding.coeWithTop_apply, meromorphicOrderAt_const_ofNat, WithBotTop.rec_bot, CategoryTheory.Triangulated.TStructure.eTruncGEπ_naturality_assoc, OrderIso.withTopCongr_apply, Finset.min_zero, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, WithTop.continuousOn_untopD, WithTop.toDual_top, ENat.some_eq_coe, MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable', CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₂, OrderIso.withTopCongr_refl, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app, ContDiff.sigmoid, WithTop.denselyOrdered, tendsto_cobounded_iff_meromorphicOrderAt_neg, WithTop.pred_untop, WithTop.lt_iff_exists_coe_btwn', meromorphicOrderAt_const, ValueDistribution.characteristic_mul_top_le, WithTop.charZero, MeasureTheory.hittingAfter_bot_le_iff, Finset.min_eq_inf_withTop, MeasureTheory.IsStoppingTime.add, Padic.AddValuation.map_one, WithTop.mul_def, MeasureTheory.IsStoppingTime.measurableSet, MeasureTheory.IsStoppingTime.measurableSet_gt, WithTop.ofDual_symm, WithTop.top_mul', Field.Emb.Cardinal.directed_filtration, ValueDistribution.logCounting_zero_mul_le, WithTop.IsWellOrder.gt, MeasureTheory.smul_le_stoppedValue_hittingBtwn, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, WithTop.untop₀_natCast, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₃, WithTop.Ioc_coe_coe, List.minimum_of_length_pos_le_iff, Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, contMDiff_addInvariantVectorField, WithTop.Ico_coe_top, ValueDistribution.proximity_zero_mul_le, CategoryTheory.Triangulated.TStructure.instIsIsoMapObjEIntFunctorETruncLTAppETruncLTι, MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_range', MeasureTheory.isStoppingTime_piecewise_const, ENat.natCast_le_of_coe_top_le_withTop, HahnSeries.orderTop_sub_pos, WithTop.untopA_lt_iff, WithTop.coe_sup, MeasureTheory.IsStoppingTime.iInf, WithBotTop.coe_le_coe, WithTop.lt_toDual_iff, MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt, WithTop.one_eq_map_iff, meromorphicOrderAt_mul, WithTop.coe_lt_top, WithTop.untop₀_mul, WithTop.Ici_coe, LatticeHom.coe_withTopWithBot, HahnSeries.SummableFamily.binomialFamily_orderTop_pos, meromorphicOrderAt_add_of_ne, MeasureTheory.StronglyAdapted.isStoppingTime_upperCrossingTime, instLieGroupOfNatWithTopENatOfIsTopologicalGroup, Tropical.instNoZeroDivisorsWithTop, WithTop.iInf_empty, MeasureTheory.IsStoppingTime.add_const', WithTop.preimage_coe_Iio_top, contMDiff_mulInvariantVectorField, WithTop.lt_def', WithTop.le_toDual_iff, ENat.coe_top_add_one, WithTop.le_def, WithTop.untop₀_zero, WithBot.ofDual_le_iff, CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdIntCoreE₂Cohomological, WithTop.untop_le_untop_iff, instContMDiffInv₀OfNatWithTopENatOfContinuousInv₀, contDiff_one_iff_fderiv, contMDiff_equivTangentBundleProd_symm, MvPowerSeries.min_lexOrder_le, ValueDistribution.logCounting_pow_top, WithTop.addLECancellable_coe, ENat.monotone_map_iff, AddHom.withTopMap_apply, contDiff_nat_succ_iff_contDiff_one_iteratedDeriv, contDiff_zero, WithTop.measurable_coe, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToLTGE_app, TopologicalSpace.instSecondCountableTopologyWithTop, WithTop.not_top_lt, Real.contDiffAt_rpow_const_of_le, WithTop.pow_right_strictMono, CategoryTheory.Triangulated.TStructure.isIso_eTruncGE_obj_map_truncGEπ_app, CategoryTheory.Triangulated.TStructure.eTruncLTLTToLT_app, MeasureTheory.hittingAfter_mono, LatticeHom.withTopWithBot_id, WithTop.eq_top_iff_forall_gt, Finset.min_union, WithTop.Ioo_coe_top, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₁, ValueDistribution.proximity_pow_zero, WithTop.untop₀_min, WithTop.top_mul, WithTop.map_eq_top_iff, WithTop.IsWellOrder.lt, contMDiff_infty, WithTop.sInf_empty, contDiffOn_nat_iff_continuousOn_differentiableOn_deriv, IsManifold.instLEInftyOfNatWithTopENat_2, WithTop.one_lt_top, ZeroHom.withTopMap_apply, Nat.cast_withTop, ValueDistribution.logCounting_coe_eq_logCounting_sub_const_zero, ValueDistribution.proximity_coe_eq_proximity_sub_const_zero, WithTop.exists_le_coe, BoxIntegral.integrable_of_continuousOn, CategoryTheory.Triangulated.TStructure.eTruncGEπ_bot, Padic.addValuation.apply, MeasureTheory.IsStoppingTime.measurableSet_ge', MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable, WithTop.untopD_top, ValueDistribution.logCounting_add_top_le, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality_assoc, WithTop.map_id, HahnSeries.le_orderTop_of_leadingCoeff_eq, TopologicalSpace.instOrderTopologyWithTop, contDiffWithinAt_nat, WithTop.coe_sSup, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom_inv_id_app_assoc, WithTop.preimage_coe_top, BoxIntegral.unitPartition.integralSum_eq_tsum_div, ENat.add_one_natCast_le_withTop_of_lt, MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB, ValueDistribution.logCounting_mul_zero_eventuallyLE, ValueDistribution.logCounting_top, WithTop.preimage_coe_Ici, CategoryTheory.Triangulated.TStructure.instAdditiveObjEIntFunctorETruncLT, MeasureTheory.IsStoppingTime.min, le_minSmoothness, contDiffOn_infty, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₂, MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj, WithTop.image_coe_Ioc, HahnSeries.orderTop_one, ENat.map_natCast_eq_zero, tangentBundle_model_space_coe_chartAt, meromorphicOrderAt_eq_top_iff, LatticeHom.withTopWithBot_comp, WithBot.map_ofDual, contDiff_iff_forall_nat_le, MeasureTheory.IsStoppingTime.measurableSet_le_stopping_time, WithTop.instOrderedSub, CategoryTheory.Triangulated.TStructure.spectralObject_ω₁, ValueDistribution.logCounting_mul_top_eventuallyLE, WithTop.one_lt_coe, contDiff_succ_iff_fderiv, WithTop.tendsto_untop, ValueDistribution.proximity_inv, contMDiffAt_mulInvariantVectorField, ENat.map_natCast_strictMono, instLieAddGroupOfNatWithTopENatOfIsTopologicalAddGroup, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₁, HahnSeries.orderTop_of_subsingleton, WithTop.mul_top, WithTop.le_iff_forall, WithTop.image_coe_Ioo, WithBot.eq_top_iff_forall_ge, fun_meromorphicOrderAt_smul, WithTop.forall, mdifferentiableAt_addInvariantVectorField, fun_meromorphicOrderAt_zpow, WithTop.coe_iInf, LatticeHom.withTopWithBot'_toFun, AddHom.ENatMap_apply, WithTop.add_eq_coe, contDiffAt_one_iff, hasFTaylorSeriesUpTo_zero_iff, HahnSeries.orderTop_mul_of_nonzero, WithTop.preimage_coe_Iio, contDiffOn_one_iff_derivWithin, WithTop.preimage_coe_Ioc, FiniteMulArchimedeanClass.withTopOrderIso_apply_coe, WithTop.mul_coe_eq_bind, WithTop.instBorelSpace, MvPowerSeries.lexOrder_mul, WithTop.Icc_coe_coe, OrderIso.withTopCongr_trans, WithTop.LinearOrderedAddCommGroup.sub_top, CategoryTheory.Triangulated.TStructure.ω₁_map, ENat.map_top, WithTop.coe_le_zero, CategoryTheory.Triangulated.TStructure.eTruncGEπ_naturality, CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₂, WithTop.untop₀_nonneg, meromorphicOrderAt_add, Tropical.mul_eq_zero_iff, WithBot.ofDual_apply_coe, CategoryTheory.Triangulated.TStructure.isZero_eTruncGE_obj_obj, WithTop.monotone_map_iff, instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, WithTop.strictMono_map_iff, WithTop.untop_zero, WithTop.Ioo_coe_coe, WithTop.Ioo_coe, MeasureTheory.IsStoppingTime.measurableSet_inter_le_const_iff, contDiff_all_iff_nat, contDiffOn_succ_of_fderivWithin, WithTop.map_sub, WithTop.coe_eq_zero, Finset.min_le, WithTop.untop₀_top, MeasureTheory.stoppedProcess_eq_stoppedValue_apply, HahnSeries.zero_lt_orderTop_of_order, Equiv.withTopCongr_trans, ValueDistribution.isBigO_characteristic_sub_characteristic_shift, MvPowerSeries.le_lexOrder_iff, List.minimum_append, WithTop.ofDual_apply_top, AddLECancellable.withTop, LatticeHom.withTop_apply, contDiffOn_omega_iff_analyticOn, HahnSeries.addVal_le_of_coeff_ne_zero, mdifferentiable_mulInvariantVectorField, MeasureTheory.AEContinuous.hasBoxIntegral, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac, CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToGELT, AddMonoidHom.withTopMap_apply, WithTop.orderIsoSumLexPUnit_toLex, ODE.contDiffOn_nat_picard_Icc, MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time_min, contDiffWithinAt_zero, ValueDistribution.characteristic_sub_characteristic_eq_proximity_sub_proximity, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, Order.height_coe_withTop, contMDiff_zero_iff, WithTop.untopD_zero_mul, WithTop.preimage_coe_Ico, WithBot.toDual_map, contDiffOn_nat_iff_continuousOn_differentiableOn, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj_assoc, ValueDistribution.logCounting_sub_const, ContDiff.norm_rpow, WithTop.eq_top_iff_forall_ne, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₁, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_inv_hom_id_app_assoc, MeasureTheory.IsStoppingTime.measurableSet_lt, ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zero, BoxIntegral.integrable_of_bounded_and_ae_continuous, meromorphicOrderAt_const_natCast, WithTop.orderIsoSumLexPUnit_symm_inl, instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold, Monotone.withTop_map, Finset.min_one, AnalyticAt.meromorphicOrderAt_nonneg, MeasureTheory.stoppedValue_lowerCrossingTime, WithTop.isOpenEmbedding_coe, WithTop.add_lt_top, ContinuousMultilinearMap.hasFTaylorSeriesUpTo_iteratedFDeriv, BoxIntegral.BoxAdditiveMap.volume_apply, WithTop.le_of_add_le_add_right, BoxIntegral.integral_nonneg, MeromorphicOn.isClopen_setOf_meromorphicOrderAt_eq_top, ENat.map_eq_top_iff, WithBot.le_toDual_iff, MeasureTheory.IsStoppingTime.measurableSet_lt_of_pred, WithTop.sub_ne_top_iff, WithTop.Iic_coe, WithTop.LinearOrderedAddCommGroup.sub_eq_top_iff, contMDiff_vectorSpace_iff_contDiff, WithTop.ofDual_lt_ofDual_iff, meromorphicOrderAt_id, ValueDistribution.characteristic_sub_characteristic_inv_at_zero, contDiff_bernoulliFun, WithBot.toDual_bot, MeasureTheory.IsStoppingTime.measurableSet_eq_le, EuclideanSpace.instIsManifoldSphere, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₂, WithTop.continuous_coe, TangentBundle.coordChange_model_space, MeasureTheory.hittingAfter_def, ValueDistribution.proximity_sum_top_le, WithTop.toDualBotEquiv_symm_top, WithTop.image_coe_Ico, Associates.mem_factorSet_some, instContMDiffInv₀OfNatWithTopENat, WithTop.iInf_coe_eq_top, CategoryTheory.Triangulated.TStructure.triangleω₁δ_map_hom₃, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable', RingHom.ENatMap_apply, MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable, hasFTaylorSeriesUpToOn_zero_iff, WithTop.pow_lt_top, Finset.le_min, WithTop.toDual_lt_iff, LatticeHom.withTop_toFun, MeasureTheory.IsStoppingTime.measurableSet_le, WithTop.lt_iff_exists_coe_btwn, CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdNatCoreE₂HomologicalNat, WithTop.coe_covBy_top, WithTop.lt_untop_iff, tendsto_nhds_iff_meromorphicOrderAt_nonneg, WithTop.coe_mul_eq_bind, OrderIso.withTopCongr_symm, CategoryTheory.Triangulated.TStructure.instIsGEObjEIntFunctorETruncGE, CategoryTheory.Abelian.SpectralObject.isZero₁_of_isFirstQuadrant, contDiffOn_succ_iff_fderiv_of_isOpen, CategoryTheory.Triangulated.TStructure.eTruncGEπ_top, WithTop.add_lt_add_right, WithTop.coe_covBy_coe, MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le, meromorphicOrderAt_pow_id_sub_const, HahnSeries.lt_orderTop_single, ValueDistribution.proximity_mul_zero_le, WithTop.map_zero, WithTop.add_lt_add_of_lt_of_le, ENat.map_natCast_mul, MeasureTheory.stoppedValue_piecewise_const, hasFTaylorSeriesUpToOn_succ_iff_right, WithTop.map_eq_natCast_iff, contDiff_nat_iff_iteratedDeriv, LatticeHom.withTop'_toFun, Padic.AddValuation.map_add, HahnSeries.orderTop_le_of_coeff_ne_zero, instIsManifoldMinSmoothnessOfNatWithTopENat_1, meromorphicOrderAt_inv, WithTop.prod_eq_top, meromorphicOrderAt_fun_prod, CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTιTopEInt, ValueDistribution.proximity_add_top_le, CategoryTheory.Abelian.SpectralObject.isZero₁_of_isThirdQuadrant, WithTop.pred_eq_top, Order.krullDim_WithTop, List.minimum_nil, contDiffPointwiseHolderAt_iff, WithTop.measurable_untopA, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac'_assoc, WithTop.existsAddOfLE, MeasureTheory.hittingAfter_eq_top_iff, Finset.min_empty, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac_assoc, ValueDistribution.logCounting_add_analyticOn, FiniteMulArchimedeanClass.withTopOrderIso_symm_apply, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_coe, WithTop.coe_sSup', meromorphicNFAt_iff_analyticAt_or, MeasureTheory.IsStoppingTime.measurable, MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_time, WithTop.coe_sInf', MeasureTheory.IsStoppingTime.measurableSet_ge, WithTop.eq_top_iff_forall_ge, WithTop.coe_zero, Field.Emb.Cardinal.equivSucc_coherence, WithBot.toDual_apply_bot, WithTop.orderIsoSumLexPUnit_top, WithTop.subtypeOrderIso_symm_apply, Tropical.instNontrivialWithTopOfZero, instContMDiffVectorBundleOfNatWithTopENat, WithTop.zeroLEOneClass, contDiffWithinAt_omega_iff_analyticWithinAt, contMDiff_smul, trivializationAt_model_space_apply, hasFTaylorSeriesUpToOn_top_iff, Real.contDiffAt_arcsin_iff, Equiv.withTopSubtypeNe_symm_apply_coe, WithTop.addLeftReflectLT, WithTop.untop₀_add, WithTop.iSup_coe_lt_top, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom_inv_id_app, MeasureTheory.stoppedValue_stoppedProcess_apply, WithTop.image_coe_Iic, contDiffOn_zero, WithTop.coe_one, WithTop.addRightReflectLT, CategoryTheory.Triangulated.TStructure.spectralObjectFunctor_map_hom, HahnSeries.orderTop_lt_top, untrop_sum, Equiv.withTopCongr_apply, ValueDistribution.characteristic_sub_characteristic_inv_le, WithTop.instUncountable, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₂, ENat.map_natCast_injective, WithTop.ge_of_forall_gt_iff_ge, hasFTaylorSeriesUpTo_succ_nat_iff_right, Order.coheight_coe_withTop, MeasureTheory.StronglyAdapted.isStoppingTime_crossing, WithBot.toDualTopEquiv_coe, CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_app_assoc, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_deg, ValueDistribution.characteristic_add_top_eventuallyLE, MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp, WithTop.add_eq_top, MeasureTheory.stoppedValue_upperCrossingTime, List.minimum_cons, HahnSeries.orderTop_mul_of_ne_zero, hasFTaylorSeriesUpToOn_succ_nat_iff_right, WithTop.untopD_zero, ENat.one_le_iff_ne_zero_withTop, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable, WithTop.pred_mono, InnerProductSpace.HarmonicOnNhd.contDiffOn, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app, HahnSeries.unit_aux, SupHom.withTop'_toFun, WithTop.map_injective, Finset.min_mem_image_coe, HahnSeries.orderTop_eq_top, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_assoc, WithTop.orderPred_coe, WithTop.add_top, contDiffWithinAt_succ_iff_hasFDerivWithinAt', CategoryTheory.Triangulated.TStructure.eTriangleLTGE_map_app_hom₁, LatticeHom.coe_withTop, contDiffOn_succ_iff_hasFDerivWithinAt, instIsContMDiffRiemannianBundleOfNatWithTopENat_2, WithTop.natCast_eq_map_iff, WithTop.Iio_coe, WithTop.untop₀_max, MeasureTheory.hittingAfter_apply_anti, BoxIntegral.norm_integral_le_of_le_const, WithTop.coe_eq_one, MeasureTheory.smul_le_stoppedValue_hitting, SupHom.withTop_toFun, AddMonoidHom.ENatMap_apply, WithTop.coe_le_iff, ValueDistribution.logCounting_add_top_eventuallyLE, MeasureTheory.stoppedValue_stoppedProcess, WithTop.coe_add_eq_top_iff, OrderEmbedding.withTopMap_apply, WithTop.ofDual_apply_coe, ValueDistribution.logCounting_mul_top_le, Ordnode.Bounded.weak_right, WithTop.iInf_coe_lt_top, CategoryTheory.Abelian.SpectralObject.isZero₂_of_isFirstQuadrant, tangentBundle_model_space_coe_chartAt_symm, WithTop.toDual_apply_top, tangentBundleModelSpaceHomeomorph_coe, CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₁, WithTop.coe_eq_bot, CategoryTheory.Triangulated.TStructure.eTruncLT_ι_top, ContDiffWithinAt.eventually_hasFTaylorSeriesUpToOn, MeasureTheory.IsStoppingTime.measurableSet_eq, MeasureTheory.measurableSet_preimage_stoppedValue_inter, IsManifold.instLEInftyOfNatWithTopENat_1, ValueDistribution.proximity_mul_top_le, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_bot, HahnSeries.addVal_apply_of_ne, WithTop.coe_pow, CategoryTheory.Triangulated.TStructure.ω₁_obj, InfHom.withTop_toFun, WithTop.image_coe_Ici, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₂, CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₂, MvPowerSeries.lexOrder_zero, ValueDistribution.characteristic_mul_zero_eventuallyLE, ValueDistribution.characteristic_pow_zero, tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero, WithTop.pred_strictMono, tangentBundleCore_coordChange_model_space, ValueDistribution.characteristic_top_mul_le, CategoryTheory.Triangulated.TStructure.eTruncLTι_naturality, List.le_minimum_of_forall_le, meromorphicOrderAt_div, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₃, contDiffOn_all_iff_nat, meromorphicOrderAt_smul, CategoryTheory.Triangulated.TStructure.isIso_eTruncLT_obj_map_truncLTπ_app, instIsManifoldMinSmoothnessOfNatWithTopENat, WithTop.isOrderedAddMonoid, contDiffGroupoid_zero_eq, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₀, ValueDistribution.logCounting_top_mul_eventually_le, ENat.LEInfty.out, HahnSeries.SummableFamily.orderTop_hsum_binomialFamily_pos, PeriodPair.order_weierstrassP, MeasureTheory.IsStoppingTime.measurableSpace_min, contDiffOn_succ_iff_deriv_of_isOpen, WithTop.image_coe_Ioi, MeasureTheory.IsStoppingTime.measurableSet_min_iff, instContMDiffMulOfNatWithTopENat, ValueDistribution.characteristic_sub_characteristic_inv, WithTop.not_top_le_coe, WithBot.toDual_le_iff, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_app_assoc, WithBot.ofDual_lt_iff, WithTop.untopD_lt_iff, Field.Emb.Cardinal.eq_bot_of_not_nonempty, InfHom.withTop'_toFun, WithBot.toDual_apply_coe, WithTop.tendsto_untopA, Manifold.riemannianEDist_def, WithBot.toDual_lt_toDual_iff, HasFTaylorSeriesUpToOn.shift_of_succ, WithTop.add_right_inj, ValueDistribution.isBigO_characteristic_sub_characteristic_inv, tangentBundleCore.isContMDiff, WithBot.ofDual_lt_ofDual_iff, WithTop.orderPred_top, WithTop.ofDual_le_ofDual_iff, WithTop.pow_lt_top_iff, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₁, contDiffOn_iff_forall_nat_le, Finset.min_eq_top, contDiff_succ_iff_fderiv_apply, LatticeHom.withTopWithBot_toFun, ENat.add_one_eq_coe_top_iff, WithTop.coe_wcovBy_top, RingHom.withTopMap_apply, MeasureTheory.stoppedProcess_eq'', WithTop.map₂_top_left, MeasureTheory.IsStoppingTime.measurableSet_le', ValueDistribution.characteristic_sum_top_le, TangentBundle.contMDiffVectorBundle, WithTop.map₂_top_right, WithTop.toDual_lt_toDual_iff, WithTop.preimage_coe_Iic, WithTop.le_of_add_le_add_left, contDiffAt_succ_iff_hasFDerivAt, WithBot.ofDual_symm_apply, WithTop.coe_bot, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_assoc, WithTop.noBotOrder, CategoryTheory.Triangulated.TStructure.isIso_eTruncLTLTIsoLT, WithTop.coe_lt_one, MeasureTheory.IsStoppingTime.measurableSet_lt_le, Tropical.add_eq_zero_iff, ValueDistribution.characteristic_add_top_le, MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable, WithTop.image_coe_Iio, List.minimum_eq_top, contDiffWithinAt_infty, WithTop.LinearOrderedAddCommGroup.coe_neg, tangentBundle_model_space_chartAt, MeasureTheory.IsStoppingTime.measurable', WithTop.denselyOrdered_iff, contMDiffAt_iff_nat, MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable_range, WithBot.toDualTopEquiv_symm_bot, WithTop.mul_top', ValueDistribution.characteristic_mul_zero_le, Finset.min_eq_bot, WithTop.map_comp_map, HahnSeries.orderTop_mul, Field.Emb.Cardinal.filtration_apply, WithTop.toDual_symm_apply, WithTop.ofDual_map, ContDiffAt.rpow_const_of_le, WithTop.map_toDual, Real.contDiffAt_rpow_const, MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const, WithTop.prod_eq_top_iff, WithTop.le_coe_iff, Finset.min_pair, ContDiff.rpow_const_of_le, trop_iInf, locallyFinsuppWithin.logCounting_divisor, MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le_const, CategoryTheory.Triangulated.TStructure.eTruncLTGELTSelfToGELT_app, WithTop.coe_lt_coe, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₁, WithTop.LinearOrderedAddCommGroup.top_sub, WithTop.lt_iff_exists, MeasureTheory.IsStoppingTime.measurableSpace_min_const, WithTop.map_eq_one_iff, Equiv.withTopCongr_refl, HahnSeries.orderTop_nsmul_le_orderTop_pow, ValueDistribution.logCounting_zero_mul_eventually_le, Finset.coe_inf_of_nonempty, MeasureTheory.ContinuousOn.hasBoxIntegral, WithTop.pred_top, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app_assoc, HahnSeries.archimedeanClassOrderIsoWithTop_apply, Finset.untrop_sum, WithTop.isEmbedding_coe, WithTop.Ioi_coe, WithTop.coe_injective, WithBot.lt_toDual_iff, WithTop.Ioc_coe, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_map_eTruncGEπ_app, WithTop.forall_coe_le_iff_le, MeasureTheory.hittingAfter_eq_sInf, MeasureTheory.stoppedProcess_eq_of_mem_finset, WithTop.untop_le_iff, Padic.AddValuation.map_zero, WithBot.toDualTopEquiv_symm_coe, WithTop.isGLB_sInf, MeasureTheory.IsStoppingTime.measurableSet_inter_le, WithTop.preimage_coe_Ioo, WithTop.toDual_symm, WithBot.ofDual_bot, MeasureTheory.le_sub_of_le_upcrossingsBefore, BoxIntegral.hasIntegral_const, WithTop.map_le_iff, WithTop.Ico_coe, WithTop.map₂_eq_top_iff, MeasureTheory.IsStoppingTime.min_const, WithTop.strictAnti_iff, Finset.inf_of_mem, ValueDistribution.characteristic_pow_top, HahnSeries.orderTop_add_le_mul, WithTop.coe_le_one, MeasureTheory.progMeasurable_min_stopping_time, WithTop.natCast_lt_top, contMDiffAt_vectorSpace_iff_contDiffAt, WithTop.top_sub_coe, Equiv.withTopCongr_symm, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_distinguished, CategoryTheory.Triangulated.TStructure.isLE_eTruncLT_obj_obj, WithTop.toDual_le_toDual_iff, WithTop.forall_le_coe_iff_le, WithTop.sum_eq_top, mdifferentiable_addInvariantVectorField, Ordnode.Bounded.weak, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range, ValueDistribution.logCounting_sum_top_eventuallyLE, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_deg, WithBotTop.coe_monotone, CategoryTheory.Triangulated.TStructure.spectralObjectFunctor_obj, contDiffAt_infty, InfHom.withTop_id, VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm, TangentBundle.symmL_model_space, WithTop.le_ofDual_iff, WithTop.canLift, WithTop.mul_lt_mul, WithBot.le_ofDual_iff, hahnEmbedding_isOrderedModule_rat, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₁, ValueDistribution.proximity_zero_of_complexValued, WithTop.top_add, CategoryTheory.Triangulated.TStructure.eTruncLT_map_app_eTruncLTι_app_assoc, WithTop.sSup_eq, HahnModule.orderTop_vAdd_le_orderTop_smul, contDiff_nat_iff_continuous_differentiable, WithTop.untop_lt_iff, WithTop.untopD_eq_iff, differentiableWithinAt_localInvariantProp, ValueDistribution.abs_characteristic_sub_characteristic_shift_eqO, Finset.le_min_iff, ValueDistribution.characteristic_zero_mul_eventually_le, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom_inv_id_app, WithTop.map_eq_zero_iff, MonoidWithZeroHom.withTopMap_apply, contDiffWithinAt_iff_forall_nat_le, WithTop.coeOrderHom_apply, WithTop.zero_eq_map_iff, ContDiffOn.one_of_succ, HahnSeries.orderTop_le_orderTop_smul, HahnSeries.orderTop_lt_iff_exists, WithTop.canonicallyOrderedAdd, FiniteArchimedeanClass.withTopOrderIso_symm_apply, ValueDistribution.proximity_const, MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range', WithTop.le_untop_iff, WithTop.toDualBotEquiv_symm_coe, LatticeHom.withTop_comp, WithTop.sInf_eq, WithTop.add_lt_add, WithTop.pow_eq_top_iff, instFiniteWithTop, WithTop.tendsto_untopD, ContDiff.one_of_succ, WithTop.lt_untopA_iff, IsAddLeftRegular.withTop, MeasureTheory.stoppedProcess_stoppedProcess', WithTop.top_mul_top, MvPowerSeries.lexOrder_eq_top_iff_eq_zero, WithTop.coe_strictMono, WithTop.add_lt_add_iff_right, WithTop.bot_eq_coe, WithTop.measurable_of_measurable_comp_coe, WithTop.coe_lt_iff, tangentBundleModelSpaceHomeomorph_coe_symm, WithTop.trichotomous.lt, contDiff_one_iff_hasFDerivAt, WithTop.mul_lt_top, instContMDiffVectorBundleOfNatWithTopENat_1, meromorphicOrderAt_pow, BoxIntegral.integralSum_sub_partitions, WithTop.LinearOrderedAddCommGroup.neg_top, WithTop.nontrivial, List.minimum_anti, WithBot.ofDual_symm, WithTop.instWellFoundedLT, WithTop.ofDual_le_iff, Measurable.withTop_coe, contMDiff_equivTangentBundleProd, HahnSeries.archimedeanClassMk_le_archimedeanClassMk_iff, instIsManifoldOfNatWithTopENatOfMinSmoothness_1, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_hom, eventuallyConst_nhdsNE_iff_meromorphicOrderAt_sub_eq_top, ValueDistribution.logCounting_add_const, MeasureTheory.contDiff_charFun, WithTop.iSup_coe_eq_top, contDiff_omega_iff_analyticOnNhd, MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le_min, WithTop.preimage_coe_Ioi, WithTop.isLUB_sSup, MeasureTheory.Measure.toBoxAdditive_apply, ContDiffWithinAt.rpow_const_of_le, WithTop.exists_lt_coe, ContDiff.iterate_deriv', WithTop.pow_lt_pow_left, WithBot.toDualTopEquiv_bot, WithTop.instIsOrderedRing, hasFTaylorSeriesUpToOn_succ_iff_left, CategoryTheory.Triangulated.TStructure.ω₁δ_app, contDiffOn_succ_iff_fderivWithin, ENat.map_natCast_nonneg, WithTop.tendsto_coe_atTop, WithBot.toDual_lt_iff, WithTop.Icc_coe, Real.contDiff_rpow_const_of_le, ValueDistribution.characteristic_zero_mul_le, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₃, MeasureTheory.IsStoppingTime.measurableSet_gt', WithTop.noMinOrder, ContDiffPointwiseHolderAt.contDiffAt, MeasureTheory.hittingAfter_empty, LatticeHom.withTop_id, WithBotTop.rec_top, hasFTaylorSeriesUpTo_top_iff, HahnSeries.SummableFamily.powers_toFun, WithTop.untopA_le_iff, WithTop.add_coe_eq_top_iff, WithTop.top_mem_insertTop, Padic.AddValuation.map_mul, CategoryTheory.Triangulated.TStructure.eTruncGEπ_app_eTruncGE_map_app, WithTop.coe_untopD_le, WithBot.toDual_le_toDual_iff, mdifferentiableAt_mulInvariantVectorField, contDiffOn_succ_iff_fderiv_apply, instIsContMDiffRiemannianBundleOfNatWithTopENat, ValueDistribution.logCounting_top_mul_le, WithTop.one_eq_coe, MeasureTheory.stoppedValue_eq', ValueDistribution.proximity_pow_top, WithTop.ofDual_lt_iff, WithTop.coe_nonneg, HahnSeries.orderTop_self_sub_one_pos_iff, ValueDistribution.logCounting_pow_zero, ENat.map_add, WithTop.le_untopD_iff, contMDiffWithinAt_infty, contDiff_succ_iff_deriv, WithTop.exists_ne_top, WithTop.top_pow, IsManifold.instOfNatWithTopENat_1, CategoryTheory.Triangulated.TStructure.isIso_eTruncGEIsoGEGE, contDiffOn_succ_iff_derivWithin, CategoryTheory.Triangulated.TStructure.eTruncGEIsoGEGE_inv_hom_id_app, BoxIntegral.integral_const, WithTop.total_le, Finset.min_insert, HahnSeries.min_orderTop_le_orderTop_sub, contDiffAt_zero, ValueDistribution.logCounting_sum_top_le, Associates.FactorSet.coe_add, WithTop.addRightMono, fun_meromorphicOrderAt_mul, MeasureTheory.hittingAfter_le_iff, instContMDiffAddOfNatWithTopENat, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom_inv_id_app_assoc, BoxIntegral.Box.volume_apply, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₃, instContMDiffMulOfNatWithTopENatOfContinuousMul, WithTop.instIsEmptyPredOrderOfNonempty, MeasureTheory.IsStoppingTime.measurableSet_eq_top, IsManifold.instOfNatWithTopENat_2, WithTop.denselyOrdered_set_iff_subsingleton, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_top, WithTop.subtypeOrderIso_apply_coe, ENat.strictMono_map_iff, WithTop.coe_wcovBy_coe, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac', WithTop.monotone_iff, UpperHalfPlane.instIsManifoldComplexModelWithCornersSelfTopWithTopENat, WithTop.map_top, MeasureTheory.stoppedValue_stoppedProcess_ae_eq, WithTop.add_lt_add_left, List.minimum_le_of_mem', WithTop.untop_lt_untop_iff, MeasureTheory.StronglyAdapted.isStoppingTime_lowerCrossingTime, ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const, MeasureTheory.hittingAfter_apply_mono, MeasureTheory.IsStoppingTime.max, meromorphicOrderAt_zpow, WithTop.isGLB_sInf', WithTop.untop_one, WithTop.orderIsoSumLexPUnit_symm_inr, MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const, MeasureTheory.le_hittingAfter, WithTop.succ_coe_of_isMax, WithTop.top_le_iff, WithTop.ofDual_symm_apply, CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToLTGE, WithTop.top_pos, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_naturality_app, untrop_sum_eq_sInf_image, WithBot.toDual_symm_apply, WithTop.coe_pos, WithTop.map_natCast, contDiff_infty, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, meromorphicOrderAt_id_sub_const, WithTop.one_le_coe, minSmoothness_add, WithTop.mul_left_strictMono, WithTop.le_of_forall_lt_iff_le, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app_assoc, WithTop.Ioc_coe_top, HahnSeries.zero_lt_orderTop_iff, Equiv.withTopSubtypeNe_apply, MeasureTheory.IsStoppingTime.add_const, WithTop.toDual_map, List.minimum_concat, contMDiffAt_infty, WithTop.coe_le_coe, CategoryTheory.Triangulated.TStructure.instIsLEObjEIntFunctorETruncGE, WithTop.tendsto_nhds_top_iff, MeasureTheory.hittingAfter_le_of_mem, CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncGEπBotEInt, WithTop.le_def', CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₃, WithTop.coe_mul, ValueDistribution.proximity_top_mul_le, contMDiff_tangentBundleModelSpaceHomeomorph_symm, meromorphicOrderAt_of_not_meromorphicAt, WithTop.coe_top_lt, CategoryTheory.Triangulated.TStructure.eTruncLTι_naturality_assoc, CategoryTheory.Triangulated.TStructure.isZero_eTruncLT_obj_obj, contDiffOn_succ_of_fderiv_apply, exist_minSmoothness_le_ne_infty, Finset.min_mono, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_coe, WithTop.untopD_one, MeasureTheory.sub_eq_zero_of_upcrossingsBefore_lt, meromorphicOrderAt_const_intCast, WithTop.succ_coe, MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range, WithTop.coe_iSup, WithTop.prod_eq_top_ex_top, Real.deriv_arcsin_aux, contDiff_norm_rpow, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₀, WithTop.coe_min, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₂, MeasureTheory.IsStoppingTime.measurableSet_min_const_iff, MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff, WithTop.untop₀_eq_zero, Field.Emb.Cardinal.iSup_filtration, WithTop.coe_natCast, WithTop.continuousOn_untopA, minSmoothness_def, WithTop.preimage_coe_Ioo_top, HahnSeries.zero_le_orderTop_iff, WithBot.toDual_symm, CategoryTheory.Triangulated.TStructure.instIsGEObjEIntFunctorETruncLT, IsMin.withTop, BoxIntegral.integrable_of_bounded_and_ae_continuousWithinAt, IsAddRightRegular.withTop, WithTop.addLeftMono, WithTop.coe_inf, WithTop.coe_sub, MvPowerSeries.lexOrder_le_of_coeff_ne_zero, OrderHom.withTopMap_coe, WithTop.strictMono_iff, CategoryTheory.Triangulated.TStructure.eTruncLT_ι_bot, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_mor₂, fun_meromorphicOrderAt_inv, WithTop.untopD_eq_untopD_iff, WithTop.none_eq_top, SupHom.withTop_id, WithTop.toDual_le_iff, WithTop.measurable_untopD, ValueDistribution.characteristic_top_mul_eventually_le, BoxIntegral.norm_integral_le_of_norm_le, WithTop.some_mem_insertTop, CategoryTheory.Triangulated.TStructure.eTruncGEδLT_coe, ContDiffPointwiseHolderAt.zero_exponent_iff, CategoryTheory.Abelian.SpectralObject.isZero₂_of_isThirdQuadrant, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₀, HahnSeries.orderTop_smul_not_lt, IsManifold.instLEInftyCastWithTopENat, WithTop.ofDual_top, WithTop.trichotomous.gt, HahnSeries.addVal_apply, WithTop.Icc_coe_top, CategoryTheory.Triangulated.TStructure.instAdditiveObjEIntFunctorETruncGE, WithTop.lt_ofDual_iff, OrderIso.withTopCongr_symm_apply, CategoryTheory.Triangulated.TStructure.ω₁δ_naturality, WithTop.coe_add, MeasureTheory.stoppedValue_eq_of_mem_finset, WithTop.image_coe_Icc, CategoryTheory.Triangulated.TStructure.instIsIsoAppETruncLTιObjEIntFunctorETruncLT, WithTop.instNoZeroDivisors, WithTop.untop₀_le_untop₀_iff, ValueDistribution.characteristic_sum_top_eventuallyLE, exists_continuousLinearEquiv_fderiv_symm_eq, WithTop.continuous_untop, WithTop.untopD_add, contMDiffOn_vectorSpace_iff_contDiffOn, List.minimum_le_coe_iff, CategoryTheory.Triangulated.TStructure.isGE_eTruncGE_obj_obj, WithTop.zero_eq_coe, ValueDistribution.log_counting_zero_sub_logCounting_top, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_top, HahnSeries.orderTop_zero, CategoryTheory.Triangulated.TStructure.instIsLEObjEIntFunctorETruncLT, WithTop.preimage_coe_Icc, WithTop.untop₀_neg, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality_assoc, Manifold.exists_lt_of_riemannianEDist_lt, MeasureTheory.IsStoppingTime.measurable_of_le, CategoryTheory.Triangulated.TStructure.eTruncLT_obj_map_eTruncLTι_app_eTruncLT_map_app, CategoryTheory.Triangulated.TStructure.eTruncGE_obj_bot, WithBotTop.coe_lt_coe, meromorphicOrderAt_prod, WithTop.coe_sum, WithTop.le_coe, AddMonoidAlgebra.infDegree_withTop_some_comp, ValueDistribution.abs_characteristic_sub_characteristic_shift_le, MeasureTheory.IsStoppingTime.biInf, contMDiffOn_zero_iff, CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₃, MvPowerSeries.le_lexOrder_mul, inTangentCoordinates_model_space, HahnSeries.mem_orderTopSubOnePos_iff, exists_continuousLinearEquiv_fderivWithin_symm_eq, CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₁, ValueDistribution.logCounting_isBigO_one_iff_analyticOnNhd, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_obj₃, minSmoothness_monotone, CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom, MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable', WithTop.sub_top, WithTop.addLECancellable_of_lt_top, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₃, WithTop.mul_right_strictMono, WithTop.sum_lt_top, contMDiffWithinAt_iff_nat, ContDiffPointwiseHolderAt.zero_order_iff, WithTop.LinearOrderedAddCommGroup.coe_sub, MeasureTheory.hittingAfter_anti, ValueDistribution.logCounting_inv, MeasureTheory.IsStoppingTime.measurableSet_stopping_time_le, Real.contDiffAt_arccos_iff, WithTop.addLECancellable_of_ne_top, ENat.natCast_lt_of_coe_top_le_withTop, WithTop.add_lt_add_iff_left, WithTop.lt_top_iff_ne_top, WithTop.coe_addHom, WithTop.preimage_coe_Ico_top, HahnSeries.min_orderTop_le_orderTop_add, WithTop.addLECancellable_iff_ne_top, ValueDistribution.proximity_top, MeasureTheory.hittingAfter_lt_iff, hasFTaylorSeriesUpToOn_top_iff_add, CategoryTheory.Abelian.SpectralObject.IsThirdQuadrant.isZero₁, MeasureTheory.IsStoppingTime.piecewise_of_le, MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le, Manifold.exists_lt_locally_constant_of_riemannianEDist_lt, InfHom.withTop_comp, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₂, inCoordinates_tangent_bundle_core_model_space, WithTop.succ_coe_of_not_isMax, WithTop.le_untopA_iff, List.not_lt_minimum_of_mem', FiniteArchimedeanClass.withTopOrderIso_apply_coe, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_map_hom₁, trop_sInf_image, MeasureTheory.IsStoppingTime.measurableSet_lt', WithTop.nhds_coe, WithTop.instCountable, WithTop.add_le_add_iff_left, WithTop.range_coe, WithBot.ofDual_le_ofDual_iff, contMDiff_snd_tangentBundle_modelSpace, WithTop.le_of_untop₀_le_untop₀, ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage, InnerProductSpace.HarmonicContOnCl.contDiffAt, WithTop.add_lt_add_of_le_of_lt, WithTop.toDual_apply_coe, IsManifold.instOfNatWithTopENat, contDiff_sigmoid, HahnSeries.leadingCoeff_of_ne_zero, CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₂, HahnSeries.le_orderTop_iff_forall, WithTop.eq_top_of_pow, MonoidWithZeroHom.ENatMap_apply, instLieGroupOfNatWithTopENat, WithTop.coe_toDualBotEquiv, WithTop.isLUB_sSup', List.trop_minimum, MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range', WithTop.add_left_inj, WithBot.map_toDual, ValueDistribution.characteristic_mul_top_eventuallyLE, CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_naturality, MeasureTheory.IsStoppingTime.measurableSet_eq', WithTop.exists, WithTop.coe_lt_zero, contMDiffOn_infty, MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff, WithTop.map_one, contDiff_succ_iff_hasFDerivAt, WithTop.toDualBotEquiv_top, fun_meromorphicOrderAt_pow, MeromorphicAt.meromorphicOrderAt_comp, hahnEmbedding_isOrderedAddMonoid, WithTop.coe_sInf, MvPowerSeries.lexOrder_mul_ge, contDiff_one_iff_deriv, CategoryTheory.Triangulated.TStructure.eTruncGEToGEGE_app, MeasureTheory.IsStoppingTime.max_const, ValueDistribution.logCounting_mul_zero_le, contDiffWithinAt_succ_iff_hasFDerivWithinAt, SupHom.withTop_comp, WithTop.range_eq, StrictMono.withTop_map, WithTop.eq_bot_iff_forall_le, WithTop.lt_iff_exists_coe, Finset.min_mem_insert_top_image_coe, WithTop.coe_nsmul, WithTop.untopD_le_iff, CategoryTheory.Triangulated.TStructure.eTruncLT_map_eq_truncLTι, hahnEmbedding_isOrderedModule, WithTop.add_le_add_iff_right, MeasureTheory.stoppedValue_piecewise_const', WithTop.mul_eq_top_iff, WithBot.ofDual_apply_bot, WithTop.map_add, CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdNatCoreE₂CohomologicalNat, MeasureTheory.stoppedProcess_eq_stoppedValue, CategoryTheory.Triangulated.TStructure.spectralObject_δ, WithTop.untopD_eq_self_iff bridge: BoxIntegral.hasIntegralIndicatorConst, MeasureTheory.SimpleFunc.hasBoxIntegral, MeasureTheory.IntegrableOn.hasBoxIntegral, BoxIntegral.HasIntegral.of_aeEq_zero, BoxIntegral.HasIntegral.congr_ae, MeasureTheory.SimpleFunc.box_integral_eq_integral

---

← Back to Index