Lemmas

📁 Source: Mathlib/Topology/Instances/NNReal/Lemmas.lean

Statistics

Metric	Count
Definitions realToNNReal, powOrderIso, powOrderIso	3
Theorems realToNNReal_apply, ofReal_map_toNNReal, iSup_pow, iSup_pow_of_ne_zero, iSup₂_pow_of_ne_zero, toNNReal, coe_tsum, coe_tsum_of_nonneg, comap_coe_atTop, hasSum_coe, hasSum_nat_add_iff, hasSum_real_toNNReal_of_nonneg, iInf_real_pos_eq_iInf_nnreal_pos, iSup_pow, iSup_pow_of_ne_zero, isOpen_Ico_zero, map_coe_atTop, map_coe_nhdsGE, map_coe_nhdsGT, nhds_zero, nhds_zero_basis, sum_add_tsum_nat_add, summable_coe, summable_comp_injective, summable_mk, summable_nat_add, summable_nat_add_iff, tendsto_atTop_zero_of_summable, tendsto_coe, tendsto_coe', tendsto_coe_atTop, tendsto_cofinite_zero_of_summable, tendsto_of_antitone, tendsto_tsum_compl_atTop_zero, tsum_mul_left, tsum_mul_right, comap_toNNReal_atTop, iSup_pow, iSup_pow_of_ne_zero, map_toNNReal_atTop, tendsto_of_bddAbove_monotone, tendsto_of_bddBelow_antitone, tendsto_toNNReal_atTop, tendsto_toNNReal_atTop_iff, continuous_real_toNNReal, tendsto_real_toNNReal, tendsto_real_toNNReal_atTop	47
Total	50

ContinuousMap

Definitions

Name	Category	Theorems
realToNNReal 📖	CompOp	14 math math: SpectrumRestricts.nnreal_of_nonneg, QuasispectrumRestricts.nnreal_iff, cfcₙHom_nnreal_eq_restrict, SpectrumRestricts.nnreal_iff, nonneg_iff_isSelfAdjoint_and_spectrumRestricts, IsSelfAdjoint.sq_spectrumRestricts, cfcHom_nnreal_eq_restrict, realToNNReal_apply, QuasispectrumRestricts.nnreal_of_nonneg, ContinuousLinearMap.IsPositive.spectrumRestricts, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, SpectrumRestricts.nnreal_iff_spectralRadius_le, CStarAlgebra.nonneg_TFAE, SpectrumRestricts.nnreal_iff_nnnorm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
realToNNReal_apply 📖	mathematical	—	DFunLike.coe ContinuousMap Real NNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.instTopologicalSpace instFunLike realToNNReal Real.toNNReal	—	—

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofReal_map_toNNReal 📖	mathematical	ContinuousOn NNReal NNReal.instTopologicalSpace Set.MapsTo Real Real.toNNReal	UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.toReal	—	Continuous.comp_continuousOn continuous_subtype_val comp Continuous.continuousOn continuous_real_toNNReal

ENNReal

Definitions

Name	Category	Theorems
powOrderIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iSup_pow 📖	mathematical	—	ENNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring instCommSemiring iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder	—	pow_zero ciSup_const iSup_pow_of_ne_zero
iSup_pow_of_ne_zero 📖	mathematical	—	ENNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring instCommSemiring iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder	—	OrderIso.map_iSup
iSup₂_pow_of_ne_zero 📖	mathematical	—	ENNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring instCommSemiring iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder	—	OrderIso.map_iSup₂

HasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toNNReal 📖	mathematical	Real Real.instLE Real.instZero HasSum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal NNReal.instTopologicalSpace Real.toNNReal	—	SummationFilter.neBot_or_eq_bot CanLift.prf NNReal.canLift nonneg Real.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology instOrderTopologyReal Pi.canLift Real.toNNReal_coe Finset.sum_congr

NNReal

Definitions

Name	Category	Theorems
powOrderIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_tsum 📖	mathematical	—	toReal tsum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Function.LeftInverse.map_tsum TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity DistribMulActionSemiHomClass.toAddMonoidHomClass IsStrictOrderedRing.toCharZero instIsStrictOrderedRing Real.instIsStrictOrderedRing SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass continuous_coe continuous_real_toNNReal Real.toNNReal_coe
coe_tsum_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	tsum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace tsum_nonneg Real.partialOrder Real.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology Real.linearOrder instOrderTopologyReal NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace	—	eq tsum_nonneg Real.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology instOrderTopologyReal coe_tsum
comap_coe_atTop 📖	mathematical	—	Filter.comap NNReal Real toReal Filter.atTop Real.instPreorder PartialOrder.toPreorder instPartialOrderNNReal	—	Filter.atTop_Ici_eq instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean
hasSum_coe 📖	mathematical	—	HasSum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toReal NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace	—	Finset.sum_congr
hasSum_nat_add_iff 📖	mathematical	—	HasSum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace SummationFilter.unconditional Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Finset.sum Finset.range	—	hasSum_coe hasSum_nat_add_iff instIsTopologicalAddGroupReal
hasSum_real_toNNReal_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	HasSum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace Real.toNNReal tsum	—	HasSum.toNNReal Summable.hasSum
iInf_real_pos_eq_iInf_nnreal_pos 📖	mathematical	—	iInf Real ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Real.instLT Real.instZero NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal toReal	—	le_antisymm iInf_mono' le_rfl iInf₂_mono' LT.lt.le
iSup_pow 📖	mathematical	—	NNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	pow_zero ciSup_const iSup_pow_of_ne_zero
iSup_pow_of_ne_zero 📖	mathematical	—	NNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	OrderIso.map_ciSup'
isOpen_Ico_zero 📖	mathematical	—	IsOpen NNReal instTopologicalSpace Set.Ico PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal	—	isOpen_Iio instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopology Set.Ico_bot
map_coe_atTop 📖	mathematical	—	Filter.map NNReal Real toReal Filter.atTop PartialOrder.toPreorder instPartialOrderNNReal Real.instPreorder	—	Filter.map_val_Ici_atTop instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean
map_coe_nhdsGE 📖	mathematical	—	Filter.map NNReal Real toReal nhdsWithin instTopologicalSpace Set.Ici PartialOrder.toPreorder instPartialOrderNNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder	—	Topology.IsEmbedding.map_nhdsWithin_eq isEmbedding_coe image_coe_Ici
map_coe_nhdsGT 📖	mathematical	—	Filter.map NNReal Real toReal nhdsWithin instTopologicalSpace Set.Ioi PartialOrder.toPreorder instPartialOrderNNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instPreorder	—	Topology.IsEmbedding.map_nhdsWithin_eq isEmbedding_coe image_coe_Ioi
nhds_zero 📖	mathematical	—	nhds NNReal instTopologicalSpace instZeroNNReal iInf Filter Filter.instInfSet Filter.principal Set.Iio PartialOrder.toPreorder instPartialOrderNNReal	—	nhds_bot_order instOrderTopology iInf_congr_Prop
nhds_zero_basis 📖	mathematical	—	Filter.HasBasis NNReal nhds instTopologicalSpace instZeroNNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal Set.Iio	—	nhds_bot_basis instOrderTopology
sum_add_tsum_nat_add 📖	mathematical	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace SummationFilter.unconditional	tsum Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Finset.sum Finset.range	—	Summable.sum_add_tsum_nat_add' TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopology UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity IsTopologicalSemiring.toContinuousAdd instIsTopologicalSemiring summable_nat_add_iff
summable_coe 📖	mathematical	—	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace toReal NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace	—	SummationFilter.neBot_or_eq_bot HasSum.nonneg Real.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology instOrderTopologyReal hasSum_coe Finset.sum_congr
summable_comp_injective 📖	—	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace SummationFilter.unconditional	—	—	summable_coe Summable.comp_injective instIsUniformAddGroupReal Real.instCompleteSpace
summable_mk 📖	mathematical	Real Real.instLE Real.instZero	Summable Nonneg.addCommMonoid Real.instAddCommMonoid Real.instPreorder IsOrderedAddMonoid.toAddLeftMono Real.partialOrder Real.instIsOrderedAddMonoid instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid summable_coe
summable_nat_add 📖	—	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace SummationFilter.unconditional	—	—	summable_comp_injective add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd
summable_nat_add_iff 📖	mathematical	—	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace SummationFilter.unconditional	—	summable_coe summable_nat_add_iff instIsTopologicalAddGroupReal
tendsto_atTop_zero_of_summable 📖	mathematical	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace SummationFilter.unconditional	Filter.Tendsto Filter.atTop Nat.instPreorder nhds instZeroNNReal	—	Nat.cofinite_eq_atTop tendsto_cofinite_zero_of_summable
tendsto_coe 📖	mathematical	—	Filter.Tendsto Real toReal nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal instTopologicalSpace	—	tendsto_subtype_rng
tendsto_coe' 📖	mathematical	—	Filter.Tendsto Real toReal nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal instTopologicalSpace Real.instLE Real.instZero	—	ge_of_tendsto' instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal tendsto_coe
tendsto_coe_atTop 📖	mathematical	—	Filter.Tendsto Real toReal Filter.atTop Real.instPreorder NNReal PartialOrder.toPreorder instPartialOrderNNReal	—	Filter.tendsto_Ici_atTop instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean
tendsto_cofinite_zero_of_summable 📖	mathematical	Summable NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace SummationFilter.unconditional	Filter.Tendsto Filter.cofinite nhds instZeroNNReal	—	Summable.tendsto_cofinite_zero instIsTopologicalAddGroupReal
tendsto_of_antitone 📖	mathematical	Antitone NNReal Nat.instPreorder PartialOrder.toPreorder instPartialOrderNNReal	Filter.Tendsto Filter.atTop nhds instTopologicalSpace	—	tendsto_atTop_ciInf LinearOrder.infConvergenceClass instOrderTopology
tendsto_tsum_compl_atTop_zero 📖	mathematical	—	Filter.Tendsto Finset NNReal tsum Finset.instMembership NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace SummationFilter.unconditional Filter.atTop PartialOrder.toPreorder Finset.partialOrder nhds instZeroNNReal	—	coe_tsum tendsto_tsum_compl_atTop_zero instIsTopologicalAddGroupReal
tsum_mul_left 📖	mathematical	—	tsum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	eq tsum_mul_left instIsTopologicalSemiring TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopology UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity coe_tsum
tsum_mul_right 📖	mathematical	—	tsum NNReal NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instTopologicalSpace Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	eq tsum_mul_right instIsTopologicalSemiring TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopology UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity coe_tsum

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_toNNReal_atTop 📖	mathematical	—	Filter.comap Real NNReal toNNReal Filter.atTop PartialOrder.toPreorder instPartialOrderNNReal instPreorder	—	le_antisymm Filter.HasBasis.ge_iff Filter.atTop_basis_Ioi' instIsDirectedOrder instIsOrderedRing instArchimedean instNoMaxOrderOfNontrivial instNontrivial Filter.mp_mem Filter.preimage_mem_comap Filter.Ioi_mem_atTop instNoTopOrderOfNoMaxOrder IsStrictOrderedRing.toNoMaxOrder NNReal.instIsStrictOrderedRing Filter.univ_mem' toNNReal_lt_toNNReal_iff_of_nonneg LT.lt.le Filter.Tendsto.le_comap tendsto_real_toNNReal_atTop
iSup_pow 📖	mathematical	Real instLE instZero	Monoid.toNatPow instMonoid iSup instSupSet	—	CanLift.prf Pi.canLift NNReal.canLift NNReal.iSup_pow
iSup_pow_of_ne_zero 📖	mathematical	Real instLE instZero	Monoid.toNatPow instMonoid iSup instSupSet	—	isEmpty_or_nonempty iSup_of_isEmpty zero_pow iSup_pow
map_toNNReal_atTop 📖	mathematical	—	Filter.map Real NNReal toNNReal Filter.atTop instPreorder PartialOrder.toPreorder instPartialOrderNNReal	—	NNReal.map_coe_atTop Function.LeftInverse.filter_map toNNReal_coe
tendsto_of_bddAbove_monotone 📖	mathematical	BddAbove Real instLE Set.range Monotone Nat.instPreorder instPreorder	Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace	—	tendsto_atTop_ciSup LinearOrder.supConvergenceClass instOrderTopologyReal
tendsto_of_bddBelow_antitone 📖	mathematical	BddBelow Real instLE Set.range Antitone Nat.instPreorder instPreorder	Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace	—	tendsto_atTop_ciInf LinearOrder.infConvergenceClass instOrderTopologyReal
tendsto_toNNReal_atTop 📖	mathematical	—	Filter.Tendsto Real NNReal toNNReal Filter.atTop instPreorder PartialOrder.toPreorder instPartialOrderNNReal	—	tendsto_toNNReal_atTop_iff Filter.tendsto_id
tendsto_toNNReal_atTop_iff 📖	mathematical	—	Filter.Tendsto NNReal toNNReal Filter.atTop PartialOrder.toPreorder instPartialOrderNNReal Real instPreorder	—	comap_toNNReal_atTop Filter.tendsto_comap_iff

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_real_toNNReal 📖	mathematical	—	Continuous Real NNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NNReal.instTopologicalSpace Real.toNNReal	—	Continuous.max OrderTopology.to_orderClosedTopology instOrderTopologyReal continuous_id continuous_const
tendsto_real_toNNReal 📖	mathematical	Filter.Tendsto Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	NNReal Real.toNNReal NNReal.instTopologicalSpace	—	Filter.Tendsto.comp Continuous.tendsto continuous_real_toNNReal
tendsto_real_toNNReal_atTop 📖	mathematical	—	Filter.Tendsto Real NNReal Real.toNNReal Filter.atTop Real.instPreorder PartialOrder.toPreorder instPartialOrderNNReal	—	Eq.le Real.map_toNNReal_atTop

---

← Back to Index