Lemmas

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

Statistics

Metric	Count
Definitions `neBotTopHomeomorphReal`	1
Theorems `ereal_toENNReal`, `ereal_toENNReal`, `ereal_toENNReal`, `ereal_toENNReal`, `const_mul`, `mul`, `mul_const`, `add_iInf_le_iInf_add`, `continuousAt_add`, `continuousAt_add_bot_bot`, `continuousAt_add_bot_coe`, `continuousAt_add_coe_bot`, `continuousAt_add_coe_coe`, `continuousAt_add_coe_top`, `continuousAt_add_top_coe`, `continuousAt_add_top_top`, `continuousAt_mul`, `continuousOn_toReal`, `continuous_coe_ennreal_iff`, `continuous_coe_iff`, `continuous_toENNReal`, `iSup_add_le_add_iSup`, `isClosedEmbedding_coe_ennreal`, `isEmbedding_coe`, `isEmbedding_coe_ennreal`, `isOpenEmbedding_coe`, `le_liminf_add`, `le_liminf_mul`, `le_limsup_add`, `le_limsup_mul`, `liminf_add_gt_of_gt`, `liminf_add_le`, `liminf_add_top_of_ne_bot`, `liminf_const_mul_of_nonneg_of_ne_top`, `liminf_const_mul_of_nonpos_of_ne_bot`, `liminf_mul_le`, `liminf_neg`, `limsup_add_bot_of_ne_top`, `limsup_add_le`, `limsup_add_le_of_le`, `limsup_const_mul_of_nonneg_of_ne_top`, `limsup_const_mul_of_nonpos_of_ne_bot`, `limsup_mul_le`, `limsup_neg`, `lowerSemicontinuous_add`, `mem_nhds_bot_iff`, `mem_nhds_top_iff`, `nhdsWithin_bot`, `nhdsWithin_top`, `nhds_bot`, `nhds_bot'`, `nhds_bot_basis`, `nhds_coe`, `nhds_coe_coe`, `nhds_top`, `nhds_top'`, `nhds_top_basis`, `tendsto_coe`, `tendsto_coe_atBot`, `tendsto_coe_atTop`, `tendsto_coe_ennreal`, `tendsto_coe_nhds_bot_iff`, `tendsto_coe_nhds_top_iff`, `tendsto_mul`, `tendsto_nhds_bot_iff_real`, `tendsto_nhds_top_iff_real`, `tendsto_toReal`, `tendsto_toReal_atBot`, `tendsto_toReal_atTop`, `continuous_coe_ennreal_ereal`, `continuous_coe_real_ereal`	71
Total	72

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ereal_toENNReal` 📖	mathematical	`Continuous` `EReal` `EReal.instTopologicalSpace`	`Continuous` `ENNReal` `ENNReal.instTopologicalSpace` `EReal.toENNReal`	—	`comp` `EReal.continuous_toENNReal`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ereal_toENNReal` 📖	mathematical	`ContinuousAt` `EReal` `EReal.instTopologicalSpace`	`ContinuousAt` `ENNReal` `ENNReal.instTopologicalSpace` `EReal.toENNReal`	—	`comp` `Continuous.continuousAt` `EReal.continuous_toENNReal`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ereal_toENNReal` 📖	mathematical	`ContinuousOn` `EReal` `EReal.instTopologicalSpace`	`ContinuousOn` `ENNReal` `ENNReal.instTopologicalSpace` `EReal.toENNReal`	—	`Continuous.comp_continuousOn` `EReal.continuous_toENNReal`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ereal_toENNReal` 📖	mathematical	`ContinuousWithinAt` `EReal` `EReal.instTopologicalSpace`	`ContinuousWithinAt` `ENNReal` `ENNReal.instTopologicalSpace` `EReal.toENNReal`	—	`ContinuousAt.comp_continuousWithinAt` `Continuous.continuousAt` `EReal.continuous_toENNReal`

EReal

Definitions

Name	Category	Theorems
`neBotTopHomeomorphReal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_iInf_le_iInf_add` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `iInf` `instInfSetEReal` `Pi.instAdd`	—	`le_iInf` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `iInf_le`
`continuousAt_add` 📖	mathematical	—	`ContinuousAt` `EReal` `instTopologicalSpaceProd` `instTopologicalSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal`	—	`continuousAt_add_bot_bot` `continuousAt_add_bot_coe` `continuousAt_add_coe_bot` `continuousAt_add_coe_coe` `continuousAt_add_coe_top` `continuousAt_add_top_coe` `continuousAt_add_top_top`
`continuousAt_add_bot_bot` 📖	mathematical	—	`ContinuousAt` `EReal` `instTopologicalSpaceProd` `instTopologicalSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Bot.bot` `instBotEReal`	—	`bot_add` `Filter.Eventually.mono` `Filter.Eventually.prod_nhds` `gt_mem_nhds` `instOrderTopology` `bot_lt_coe` `zero_add` `add_lt_add`
`continuousAt_add_bot_coe` 📖	mathematical	—	`ContinuousAt` `EReal` `instTopologicalSpaceProd` `instTopologicalSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Bot.bot` `instBotEReal` `Real.toEReal`	—	`bot_add` `Filter.Eventually.mono` `Filter.Eventually.prod_nhds` `gt_mem_nhds` `instOrderTopology` `bot_lt_coe` `coe_lt_coe_iff` `lt_add_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_add_cancel` `add_lt_add`
`continuousAt_add_coe_bot` 📖	mathematical	—	`ContinuousAt` `EReal` `instTopologicalSpaceProd` `instTopologicalSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Real.toEReal` `Bot.bot` `instBotEReal`	—	`add_comm` `Filter.Tendsto.comp` `continuousAt_add_bot_coe` `Continuous.tendsto` `continuous_swap`
`continuousAt_add_coe_coe` 📖	mathematical	—	`ContinuousAt` `EReal` `instTopologicalSpaceProd` `instTopologicalSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Real.toEReal`	—	`nhds_coe_coe` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal`
`continuousAt_add_coe_top` 📖	mathematical	—	`ContinuousAt` `EReal` `instTopologicalSpaceProd` `instTopologicalSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Real.toEReal` `Top.top` `instTopEReal`	—	`add_comm` `Filter.Tendsto.comp` `continuousAt_add_top_coe` `Continuous.tendsto` `continuous_swap`
`continuousAt_add_top_coe` 📖	mathematical	—	`ContinuousAt` `EReal` `instTopologicalSpaceProd` `instTopologicalSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Top.top` `instTopEReal` `Real.toEReal`	—	`Filter.Eventually.mono` `Filter.Eventually.prod_nhds` `lt_mem_nhds` `instOrderTopology` `coe_lt_top` `coe_lt_coe_iff` `sub_one_lt` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_add_cancel` `add_lt_add`
`continuousAt_add_top_top` 📖	mathematical	—	`ContinuousAt` `EReal` `instTopologicalSpaceProd` `instTopologicalSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Top.top` `instTopEReal`	—	`Filter.Eventually.mono` `Filter.Eventually.prod_nhds` `lt_mem_nhds` `instOrderTopology` `coe_lt_top` `zero_add` `add_lt_add`
`continuousAt_mul` 📖	mathematical	—	`ContinuousAt` `EReal` `instTopologicalSpaceProd` `instTopologicalSpace` `instMul`	—	`neg_top`
`continuousOn_toReal` 📖	mathematical	—	`ContinuousOn` `EReal` `Real` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `toReal` `Compl.compl` `Set` `Set.instCompl` `Set.instInsert` `Bot.bot` `instBotEReal` `Set.instSingletonSet` `Top.top` `instTopEReal`	—	`ContinuousAt.continuousWithinAt` `tendsto_toReal`
`continuous_coe_ennreal_iff` 📖	mathematical	—	`Continuous` `EReal` `instTopologicalSpace` `ENNReal.toEReal` `ENNReal` `ENNReal.instTopologicalSpace`	—	`Topology.IsEmbedding.continuous_iff` `isEmbedding_coe_ennreal`
`continuous_coe_iff` 📖	mathematical	—	`Continuous` `EReal` `instTopologicalSpace` `Real.toEReal` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`Topology.IsEmbedding.continuous_iff` `isEmbedding_coe`
`continuous_toENNReal` 📖	mathematical	—	`Continuous` `EReal` `ENNReal` `instTopologicalSpace` `ENNReal.instTopologicalSpace` `toENNReal`	—	`continuous_iff_continuousAt` `ENNReal.tendsto_nhds_top` `Filter.mp_mem` `eventually_gt_nhds` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopology` `coe_lt_top` `Filter.univ_mem'` `toENNReal_lt_toENNReal` `coe_ennreal_nonneg` `toENNReal_coe` `ContinuousOn.continuousAt` `ContinuousOn.congr` `continuousOn_of_forall_continuousAt` `tendsto_nhds_of_eventually_eq` `Filter.HasBasis.eventually_iff` `nhds_bot_basis` `ENNReal.ofReal_zero` `toReal_nonpos` `LT.lt.le` `ContinuousAt.comp'` `Continuous.continuousAt` `ENNReal.continuous_ofReal` `continuousOn_toReal` `IsClosed.compl_mem_nhds` `Set.Finite.isClosed` `T5Space.toT1Space` `instT5Space` `Set.toFinite` `Finite.Set.finite_insert` `Finite.of_fintype` `toENNReal_of_ne_top` `compl_singleton_mem_nhds_iff`
`iSup_add_le_add_iSup` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `iSup` `instSupSetEReal` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal`	—	`iSup_le` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `le_iSup`
`isClosedEmbedding_coe_ennreal` 📖	mathematical	—	`Topology.IsClosedEmbedding` `ENNReal` `EReal` `ENNReal.instTopologicalSpace` `instTopologicalSpace` `ENNReal.toEReal`	—	`isEmbedding_coe_ennreal` `range_coe_ennreal` `isClosed_Ici` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopology`
`isEmbedding_coe` 📖	mathematical	—	`Topology.IsEmbedding` `Real` `EReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpace` `Real.toEReal`	—	`StrictMono.isEmbedding_of_ordConnected` `instOrderTopologyReal` `instOrderTopology` `coe_strictMono` `range_coe_eq_Ioo` `Set.ordConnected_Ioo`
`isEmbedding_coe_ennreal` 📖	mathematical	—	`Topology.IsEmbedding` `ENNReal` `EReal` `ENNReal.instTopologicalSpace` `instTopologicalSpace` `ENNReal.toEReal`	—	`StrictMono.isEmbedding_of_ordConnected` `ENNReal.instOrderTopology` `instOrderTopology` `coe_ennreal_strictMono` `range_coe_ennreal` `Set.ordConnected_Ici`
`isOpenEmbedding_coe` 📖	mathematical	—	`Topology.IsOpenEmbedding` `Real` `EReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpace` `Real.toEReal`	—	`isEmbedding_coe` `range_coe_eq_Ioo` `OrderTopology.to_orderClosedTopology` `instOrderTopology`
`le_liminf_add` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Pi.instAdd`	—	`add_le_of_forall_lt` `Filter.le_liminf_iff` `Filter.isCobounded_ge_of_top` `Filter.isBounded_ge_of_bot` `Filter.mp_mem` `Filter.eventually_lt_of_lt_liminf` `Filter.univ_mem'` `LT.lt.trans` `add_lt_add`
`le_liminf_mul` 📖	mathematical	`Filter.EventuallyLE` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `Pi.instZero` `instZeroEReal`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instMul` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Pi.instMul`	—	`mul_le_of_forall_lt_of_nonneg` `Filter.le_liminf_of_le` `Filter.isCobounded_ge_of_top` `Filter.Eventually.mono` `Filter.Eventually.and` `mul_nonneg` `instPosMulMono` `Filter.le_liminf_iff` `Filter.isBounded_ge_of_bot` `Filter.mp_mem` `Filter.eventually_lt_of_lt_liminf` `Set.mem_Ioo` `Filter.univ_mem'` `LT.lt.trans_le` `mul_le_mul` `instMulPosMono` `LT.lt.le` `LE.le.trans`
`le_limsup_add` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Filter.liminf` `Pi.instAdd`	—	`add_le_of_forall_lt` `Filter.le_limsup_iff` `Filter.isCobounded_le_of_bot` `Filter.isBounded_le_of_top` `Filter.Frequently.mono` `Filter.Frequently.and_eventually` `Filter.frequently_lt_of_lt_limsup` `Filter.eventually_lt_of_lt_liminf` `Filter.isBounded_ge_of_bot` `LT.lt.trans` `add_lt_add`
`le_limsup_mul` 📖	mathematical	`Filter.Frequently` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal` `Filter.EventuallyLE` `Pi.instZero`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instMul` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Filter.liminf` `Pi.instMul`	—	`Filter.eq_or_neBot` `Filter.limsup_bot` `Filter.liminf_bot` `bot_mul_top` `le_refl` `Filter.le_limsup_of_frequently_le` `Filter.isBounded_le_of_top` `Filter.Frequently.mono` `Filter.Frequently.and_eventually` `mul_nonneg` `instPosMulMono` `mul_le_of_forall_lt_of_nonneg` `Filter.le_limsup_iff` `Filter.isCobounded_le_of_bot` `Filter.frequently_lt_of_lt_limsup` `Set.mem_Ioo` `Filter.Eventually.and` `Filter.eventually_lt_of_lt_liminf` `Filter.isBounded_ge_of_bot` `LT.lt.trans_le` `mul_le_mul` `instMulPosMono` `LT.lt.le` `LE.le.trans`
`liminf_add_gt_of_gt` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal`	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Pi.instAdd`	—	`LT.lt.trans_le` `add_lt_add` `le_liminf_add`
`liminf_add_le` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Filter.limsup`	—	`le_add_of_forall_gt` `Filter.liminf_le_iff` `Filter.isCobounded_ge_of_top` `Filter.isBounded_ge_of_bot` `Filter.Frequently.mono` `Filter.Frequently.and_eventually` `Filter.frequently_lt_of_liminf_lt` `Filter.eventually_lt_of_limsup_lt` `Filter.isBounded_le_of_top` `LT.lt.trans` `add_lt_add`
`liminf_add_top_of_ne_bot` 📖	mathematical	`Filter.liminf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Top.top` `instTopEReal`	`Filter.liminf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Top.top` `instTopEReal`	—	`top_le_iff` `le_trans` `top_add_of_ne_bot` `le_refl` `le_liminf_add`
`liminf_const_mul_of_nonneg_of_ne_top` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`Filter.liminf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `instMul`	—	`mul_neg` `limsup_neg` `limsup_const_mul_of_nonneg_of_ne_top`
`liminf_const_mul_of_nonpos_of_ne_bot` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`Filter.liminf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `instMul` `Filter.limsup`	—	`neg_mul` `limsup_neg` `limsup_const_mul_of_nonneg_of_ne_top`
`liminf_mul_le` 📖	mathematical	`Filter.EventuallyLE` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `Pi.instZero` `instZeroEReal`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Pi.instMul` `instMul` `Filter.limsup`	—	`lt_of_le_of_ne` `Filter.limsup_const` `Filter.limsup_le_limsup` `Filter.isCobounded_le_of_bot` `Filter.isBounded_le_of_top` `Filter.liminf_const` `Filter.liminf_le_liminf` `Filter.isBounded_ge_of_bot` `Filter.isCobounded_ge_of_top` `le_mul_of_forall_lt` `Filter.liminf_le_iff` `Filter.Frequently.mono` `Filter.Frequently.and_eventually` `Filter.frequently_lt_of_liminf_lt` `Filter.Eventually.and` `Filter.eventually_lt_of_limsup_lt` `LE.le.trans_lt` `mul_le_mul` `instPosMulMono` `instMulPosMono` `LT.lt.le` `LE.le.trans`
`liminf_neg` 📖	mathematical	—	`Filter.liminf` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Pi.instNeg` `instNeg` `Filter.limsup`	—	`OrderIso.limsup_apply` `Filter.isBounded_le_of_top` `Filter.isCobounded_le_of_bot`
`limsup_add_bot_of_ne_top` 📖	mathematical	`Filter.limsup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Bot.bot` `instBotEReal`	`Filter.limsup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal` `Bot.bot` `instBotEReal`	—	`le_bot_iff` `LE.le.trans` `limsup_add_le` `bot_ne_top` `bot_add` `le_refl`
`limsup_add_le` 📖	mathematical	—	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal`	—	`le_add_of_forall_gt` `Filter.limsup_le_iff` `Filter.isCobounded_le_of_bot` `Filter.isBounded_le_of_top` `Filter.mp_mem` `Filter.eventually_lt_of_limsup_lt` `Filter.univ_mem'` `LT.lt.trans` `add_lt_add`
`limsup_add_le_of_le` 📖	mathematical	`EReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Preorder.toLE`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal`	—	`eq_top_or_lt_top` `add_top_of_ne_bot` `LT.lt.ne_bot` `le_top` `LE.le.trans` `limsup_add_le` `LT.lt.ne` `LE.le.trans_lt` `LT.lt.ne_top` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `LT.lt.le`
`limsup_const_mul_of_nonneg_of_ne_top` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`Filter.limsup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `instMul`	—	`LE.le.eq_or_lt` `MulZeroClass.zero_mul` `Filter.limsup_const` `mul_comm` `eq_of_le_of_ge` `Filter.limsup_le_iff` `Filter.isCobounded_le_of_bot` `Filter.isBounded_le_of_top` `lt_div_iff` `Filter.eventually_lt_of_limsup_lt` `Filter.le_limsup_iff` `div_lt_iff` `Filter.frequently_lt_of_lt_limsup`
`limsup_const_mul_of_nonpos_of_ne_bot` 📖	mathematical	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal`	`Filter.limsup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `instMul` `Filter.liminf`	—	`mul_neg` `neg_mul` `neg_neg` `limsup_neg` `limsup_const_mul_of_nonneg_of_ne_top`
`limsup_mul_le` 📖	mathematical	`Filter.Frequently` `EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `instZeroEReal` `Filter.EventuallyLE` `Pi.instZero`	`EReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderEReal` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Pi.instMul` `instMul`	—	`Filter.eq_or_neBot` `Filter.limsup_bot` `bot_le` `Filter.le_limsup_of_frequently_le` `Filter.isBounded_le_of_top` `lt_of_le_of_ne` `Filter.Eventually.frequently` `le_mul_of_forall_lt` `Filter.limsup_le_iff` `Filter.isCobounded_le_of_bot` `Filter.mp_mem` `Filter.eventually_lt_of_limsup_lt` `Filter.univ_mem'` `lt_of_le_of_lt` `lt_or_ge` `LE.le.trans` `mul_nonpos_iff` `LT.lt.le` `mul_nonneg` `instPosMulMono` `mul_le_mul` `instMulPosMono`
`limsup_neg` 📖	mathematical	—	`Filter.limsup` `EReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderEReal` `Pi.instNeg` `instNeg` `Filter.liminf`	—	`OrderIso.liminf_apply` `Filter.isBounded_ge_of_bot` `Filter.isCobounded_ge_of_top`
`lowerSemicontinuous_add` 📖	mathematical	—	`LowerSemicontinuous` `EReal` `instTopologicalSpaceProd` `instTopologicalSpace` `PartialOrder.toPreorder` `instPartialOrderEReal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instAddCommMonoidEReal`	—	`bot_add` `instIsEmptyFalse` `add_bot` `ContinuousAt.lowerSemicontinuousAt` `instOrderTopology` `continuousAt_add`
`mem_nhds_bot_iff` 📖	mathematical	—	`Set` `EReal` `Filter` `Filter.instMembership` `nhds` `instTopologicalSpace` `Bot.bot` `instBotEReal` `Real` `Set.instHasSubset` `Set.Iio` `PartialOrder.toPreorder` `instPartialOrderEReal` `Real.toEReal`	—	`Filter.HasBasis.mem_iff` `nhds_bot_basis`
`mem_nhds_top_iff` 📖	mathematical	—	`Set` `EReal` `Filter` `Filter.instMembership` `nhds` `instTopologicalSpace` `Top.top` `instTopEReal` `Real` `Set.instHasSubset` `Set.Ioi` `PartialOrder.toPreorder` `instPartialOrderEReal` `Real.toEReal`	—	`Filter.HasBasis.mem_iff` `nhds_top_basis`
`nhdsWithin_bot` 📖	mathematical	—	`nhdsWithin` `EReal` `instTopologicalSpace` `Bot.bot` `instBotEReal` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.map` `Real` `Real.toEReal` `Filter.atBot` `Real.instPreorder`	—	`Filter.HasBasis.ext` `nhdsWithin_hasBasis` `nhds_bot_basis_Iic` `instOrderTopology` `Filter.HasBasis.map` `Filter.atBot_basis` `instIsCodirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `image_coe_Iic` `Set.Iic_top` `Set.univ_inter` `CanLift.prf` `canLift` `LT.lt.ne_bot` `bot_lt_coe` `Ne.bot_lt'`
`nhdsWithin_top` 📖	mathematical	—	`nhdsWithin` `EReal` `instTopologicalSpace` `Top.top` `instTopEReal` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.map` `Real` `Real.toEReal` `Filter.atTop` `Real.instPreorder`	—	`Filter.HasBasis.ext` `nhdsWithin_hasBasis` `nhds_top_basis_Ici` `instOrderTopology` `Filter.HasBasis.map` `Filter.atTop_basis` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `image_coe_Ici` `Set.Ici_bot` `Set.univ_inter` `CanLift.prf` `canLift` `LT.lt.ne_top` `coe_lt_top` `Ne.lt_top'`
`nhds_bot` 📖	mathematical	—	`nhds` `EReal` `instTopologicalSpace` `Bot.bot` `instBotEReal` `iInf` `Filter` `Filter.instInfSet` `Filter.principal` `Set.Iio` `PartialOrder.toPreorder` `instPartialOrderEReal`	—	`nhds_bot_order` `instOrderTopology` `iInf_congr_Prop`
`nhds_bot'` 📖	mathematical	—	`nhds` `EReal` `instTopologicalSpace` `Bot.bot` `instBotEReal` `iInf` `Filter` `Real` `Filter.instInfSet` `Filter.principal` `Set.Iio` `PartialOrder.toPreorder` `instPartialOrderEReal` `Real.toEReal`	—	`Filter.HasBasis.eq_iInf` `nhds_bot_basis`
`nhds_bot_basis` 📖	mathematical	—	`Filter.HasBasis` `EReal` `Real` `nhds` `instTopologicalSpace` `Bot.bot` `instBotEReal` `Set.Iio` `PartialOrder.toPreorder` `instPartialOrderEReal` `Real.toEReal`	—	`Filter.HasBasis.to_hasBasis` `nhds_bot_basis` `instOrderTopology` `exists_rat_btwn_of_lt` `Set.Iio_subset_Iio` `LT.lt.le` `bot_lt_coe` `Set.Subset.rfl`
`nhds_coe` 📖	mathematical	—	`nhds` `EReal` `instTopologicalSpace` `Real.toEReal` `Filter.map` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`Topology.IsOpenEmbedding.map_nhds_eq` `isOpenEmbedding_coe`
`nhds_coe_coe` 📖	mathematical	—	`nhds` `EReal` `instTopologicalSpaceProd` `instTopologicalSpace` `Real.toEReal` `Filter.map` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`Topology.IsOpenEmbedding.map_nhds_eq` `Topology.IsOpenEmbedding.prodMap` `isOpenEmbedding_coe`
`nhds_top` 📖	mathematical	—	`nhds` `EReal` `instTopologicalSpace` `Top.top` `instTopEReal` `iInf` `Filter` `Filter.instInfSet` `Filter.principal` `Set.Ioi` `PartialOrder.toPreorder` `instPartialOrderEReal`	—	`nhds_top_order` `instOrderTopology` `iInf_congr_Prop`
`nhds_top'` 📖	mathematical	—	`nhds` `EReal` `instTopologicalSpace` `Top.top` `instTopEReal` `iInf` `Filter` `Real` `Filter.instInfSet` `Filter.principal` `Set.Ioi` `PartialOrder.toPreorder` `instPartialOrderEReal` `Real.toEReal`	—	`Filter.HasBasis.eq_iInf` `nhds_top_basis`
`nhds_top_basis` 📖	mathematical	—	`Filter.HasBasis` `EReal` `Real` `nhds` `instTopologicalSpace` `Top.top` `instTopEReal` `Set.Ioi` `PartialOrder.toPreorder` `instPartialOrderEReal` `Real.toEReal`	—	`Filter.HasBasis.to_hasBasis` `nhds_top_basis` `instOrderTopology` `exists_rat_btwn_of_lt` `Set.Ioi_subset_Ioi` `LT.lt.le` `coe_lt_top` `Set.Subset.rfl`
`tendsto_coe` 📖	mathematical	—	`Filter.Tendsto` `EReal` `Real.toEReal` `nhds` `instTopologicalSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`Topology.IsEmbedding.tendsto_nhds_iff` `isEmbedding_coe`
`tendsto_coe_atBot` 📖	mathematical	—	`Filter.Tendsto` `Real` `EReal` `Real.toEReal` `Filter.atBot` `Real.instPreorder` `nhds` `instTopologicalSpace` `Bot.bot` `instBotEReal`	—	`tendsto_coe_nhds_bot_iff` `Filter.tendsto_id`
`tendsto_coe_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `EReal` `Real.toEReal` `Filter.atTop` `Real.instPreorder` `nhds` `instTopologicalSpace` `Top.top` `instTopEReal`	—	`tendsto_coe_nhds_top_iff` `Filter.tendsto_id`
`tendsto_coe_ennreal` 📖	mathematical	—	`Filter.Tendsto` `EReal` `ENNReal.toEReal` `nhds` `instTopologicalSpace` `ENNReal` `ENNReal.instTopologicalSpace`	—	`Topology.IsEmbedding.tendsto_nhds_iff` `isEmbedding_coe_ennreal`
`tendsto_coe_nhds_bot_iff` 📖	mathematical	—	`Filter.Tendsto` `EReal` `Real.toEReal` `nhds` `instTopologicalSpace` `Bot.bot` `instBotEReal` `Real` `Filter.atBot` `Real.instPreorder`	—	`tendsto_nhds_bot_iff_real` `Filter.HasBasis.tendsto_right_iff` `Filter.atBot_basis_Iio` `instIsCodirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `instNoMinOrderOfNontrivial` `Real.instNontrivial`
`tendsto_coe_nhds_top_iff` 📖	mathematical	—	`Filter.Tendsto` `EReal` `Real.toEReal` `nhds` `instTopologicalSpace` `Top.top` `instTopEReal` `Real` `Filter.atTop` `Real.instPreorder`	—	`tendsto_nhds_top_iff_real` `Filter.HasBasis.tendsto_right_iff` `Filter.atTop_basis_Ioi` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `instNoMaxOrderOfNontrivial` `Real.instNontrivial`
`tendsto_mul` 📖	mathematical	—	`Filter.Tendsto` `EReal` `instMul` `nhds` `instTopologicalSpaceProd` `instTopologicalSpace`	—	`ContinuousAt.tendsto` `continuousAt_mul`
`tendsto_nhds_bot_iff_real` 📖	mathematical	—	`Filter.Tendsto` `EReal` `nhds` `instTopologicalSpace` `Bot.bot` `instBotEReal` `Filter.Eventually` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `Real.toEReal`	—	`Filter.HasBasis.tendsto_right_iff` `nhds_bot_basis`
`tendsto_nhds_top_iff_real` 📖	mathematical	—	`Filter.Tendsto` `EReal` `nhds` `instTopologicalSpace` `Top.top` `instTopEReal` `Filter.Eventually` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderEReal` `Real.toEReal`	—	`Filter.HasBasis.tendsto_right_iff` `nhds_top_basis`
`tendsto_toReal` 📖	mathematical	—	`Filter.Tendsto` `EReal` `Real` `toReal` `nhds` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`CanLift.prf` `canLift` `nhds_coe` `Filter.tendsto_map'_iff` `Filter.tendsto_id`
`tendsto_toReal_atBot` 📖	mathematical	—	`Filter.Tendsto` `EReal` `Real` `toReal` `nhdsWithin` `instTopologicalSpace` `Bot.bot` `instBotEReal` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.atBot` `Real.instPreorder`	—	`nhdsWithin_bot` `Filter.tendsto_map'_iff` `Filter.tendsto_id`
`tendsto_toReal_atTop` 📖	mathematical	—	`Filter.Tendsto` `EReal` `Real` `toReal` `nhdsWithin` `instTopologicalSpace` `Top.top` `instTopEReal` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.atTop` `Real.instPreorder`	—	`nhdsWithin_top` `Filter.tendsto_map'_iff` `Filter.tendsto_id`

EReal.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_mul` 📖	mathematical	`Filter.Tendsto` `EReal` `nhds` `EReal.instTopologicalSpace`	`Filter.Tendsto` `EReal` `EReal.instMul` `nhds` `EReal.instTopologicalSpace`	—	`by_cases` `MulZeroClass.zero_mul` `mul` `tendsto_const_nhds`
`mul` 📖	mathematical	`Filter.Tendsto` `EReal` `nhds` `EReal.instTopologicalSpace`	`Filter.Tendsto` `EReal` `EReal.instMul` `nhds` `EReal.instTopologicalSpace`	—	`Filter.Tendsto.comp` `EReal.tendsto_mul` `Filter.Tendsto.prodMk_nhds`
`mul_const` 📖	mathematical	`Filter.Tendsto` `EReal` `nhds` `EReal.instTopologicalSpace`	`Filter.Tendsto` `EReal` `EReal.instMul` `nhds` `EReal.instTopologicalSpace`	—	`mul_comm` `const_mul`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_coe_ennreal_ereal` 📖	mathematical	—	`Continuous` `ENNReal` `EReal` `ENNReal.instTopologicalSpace` `EReal.instTopologicalSpace` `ENNReal.toEReal`	—	`Topology.IsEmbedding.continuous` `EReal.isEmbedding_coe_ennreal`
`continuous_coe_real_ereal` 📖	mathematical	—	`Continuous` `Real` `EReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `EReal.instTopologicalSpace` `Real.toEReal`	—	`Topology.IsEmbedding.continuous` `EReal.isEmbedding_coe`

---

← Back to Index