Lemmas

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

Statistics

Metric	Count
Definitions `ltTopHomeomorphNNReal`, `neTopHomeomorphNNReal`, `truncateToReal`, `metricSpaceEMetricBall`	4
Theorems `edist`, `ennreal_mul`, `ennreal_mul`, `lipschitzWith_extend`, `cauchySeq_iff_le_tendsto_0`, `diam_closure`, `isClosed_closedBall`, `Icc_mem_nhds`, `const_div`, `const_mul`, `div`, `div_const`, `mul`, `mul_const`, `pow`, `sub`, `biInf_le_nhds`, `coe_range_mem_nhds`, `continuousAt_coe_iff`, `continuousAt_const_mul`, `continuousAt_mul_const`, `continuousAt_toReal`, `continuousOn_sub`, `continuousOn_sub_left`, `continuousOn_toNNReal`, `continuousOn_toReal`, `continuous_coe`, `continuous_coe_iff`, `continuous_const_mul`, `continuous_div_const`, `continuous_mul_const`, `continuous_nnreal_sub`, `continuous_ofReal`, `continuous_pow`, `continuous_sub_left`, `continuous_sub_right`, `continuous_truncateToReal`, `continuous_zpow`, `eventuallyEq_of_toReal_eventuallyEq`, `exists_countable_dense_no_zero_top`, `exists_frequently_lt_of_liminf_ne_top`, `exists_frequently_lt_of_liminf_ne_top'`, `exists_upcrossings_of_not_bounded_under`, `hasBasis_nhds_of_ne_top`, `hasBasis_nhds_of_ne_top'`, `inv_liminf`, `inv_limsup`, `isOpen_Ico_zero`, `isOpen_ne_top`, `le_liminf_mul`, `le_limsup_mul`, `le_of_forall_lt_one_mul_le`, `liminf_add_of_left_tendsto_zero`, `liminf_add_of_right_tendsto_zero`, `liminf_const_sub`, `liminf_mul_le`, `liminf_sub_const`, `liminf_toReal_eq`, `limsup_add_of_left_tendsto_zero`, `limsup_add_of_right_tendsto_zero`, `limsup_const_sub`, `limsup_mul_le'`, `limsup_sub_const`, `limsup_toReal_eq`, `monotone_truncateToReal`, `nhdsGT_coe_neBot`, `nhdsGT_nat_neBot`, `nhdsGT_ofNat_neBot`, `nhdsGT_one_neBot`, `nhdsGT_zero_neBot`, `nhdsLT_neBot`, `nhds_coe`, `nhds_of_ne_top`, `nhds_top`, `nhds_top'`, `nhds_top_basis`, `nhds_zero`, `nhds_zero_basis`, `nhds_zero_basis_Iic`, `ofNNReal_liminf`, `ofNNReal_limsup`, `tendsto_atTop`, `tendsto_atTop_zero`, `tendsto_atTop_zero_iff_le_of_antitone`, `tendsto_atTop_zero_iff_lt_of_antitone`, `tendsto_coe_nhds_top`, `tendsto_coe_sub`, `tendsto_coe_toNNReal`, `tendsto_const_sub_nhds_zero_iff`, `tendsto_finset_prod_of_ne_top`, `tendsto_inv_iff`, `tendsto_inv_nat_nhds_zero`, `tendsto_mul`, `tendsto_nat_nhds_top`, `tendsto_nhds`, `tendsto_nhds_coe_iff`, `tendsto_nhds_of_Icc`, `tendsto_nhds_top`, `tendsto_nhds_top_iff_nat`, `tendsto_nhds_top_iff_nnreal`, `tendsto_nhds_zero`, `tendsto_ofReal`, `tendsto_ofReal_atTop`, `tendsto_ofReal_nhds_top`, `tendsto_sub`, `tendsto_toNNReal`, `tendsto_toNNReal_iff`, `tendsto_toNNReal_iff'`, `tendsto_toReal`, `tendsto_toReal_iff`, `tendsto_toReal_zero_iff`, `truncateToReal_eq_toReal`, `truncateToReal_le`, `truncateToReal_nonneg`, `edist`, `closure`, `diam_closure`, `ediam_closure`, `isClosed_closedEBall`, `diam_Icc`, `diam_Ico`, `diam_Ioc`, `diam_Ioo`, `diam_eq`, `ediam_Icc`, `ediam_Ico`, `ediam_Ioc`, `ediam_Ioo`, `ediam_eq`, `continuous_edist`, `continuous_of_le_add_edist`, `edist_ne_top_of_mem_ball`, `isClosed_setOf_lipschitzOnWith`, `isClosed_setOf_lipschitzWith`, `lipschitzOnWith_closure_iff`, `nhds_eq_nhds_emetric_ball`, `tendsto_iff_edist_tendsto_0`	137
Total	141

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edist` 📖	mathematical	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Continuous` `ENNReal` `ENNReal.instTopologicalSpace` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`comp` `continuous_edist` `prodMk`
`ennreal_mul` 📖	mathematical	`Continuous` `ENNReal` `ENNReal.instTopologicalSpace`	`Continuous` `ENNReal` `ENNReal.instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`continuous_iff_continuousAt` `ENNReal.Tendsto.mul` `continuousAt`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ennreal_mul` 📖	mathematical	`ContinuousOn` `ENNReal` `ENNReal.instTopologicalSpace`	`ContinuousOn` `ENNReal` `ENNReal.instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`ENNReal.Tendsto.mul`

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lipschitzWith_extend` 📖	mathematical	`Dense` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `LipschitzWith` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `EMetricSpace.toPseudoEMetricSpace`	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `extend` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`UniformContinuous.continuous` `uniformContinuous_extend` `LipschitzWith.uniformContinuous` `isClosed_le` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Continuous.edist` `Continuous.comp'` `Continuous.fst` `continuous_id'` `Continuous.snd` `Continuous.comp` `ENNReal.continuous_const_mul` `mono` `prod` `extend_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `LipschitzWith.continuous` `IsClosed.closure_eq`

EMetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchySeq_iff_le_tendsto_0` 📖	mathematical	—	`CauchySeq` `PseudoEMetricSpace.toUniformSpace` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `Filter.Tendsto` `Filter.atTop` `nhds` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`cauchySeq_iff` `Metric.edist_le_ediam_of_mem` `Set.mem_image_of_mem` `ENNReal.tendsto_nhds_zero` `Filter.Eventually.mono` `Filter.eventually_ge_atTop` `Metric.ediam_le` `LT.lt.le` `LE.le.trans` `Filter.Tendsto.eventually` `gt_mem_nhds` `ENNReal.instOrderTopology` `Filter.Eventually.exists` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder`
`diam_closure` 📖	mathematical	—	`Metric.ediam` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`Metric.ediam_closure`
`isClosed_closedBall` 📖	mathematical	—	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `Metric.closedEBall`	—	`Metric.isClosed_closedEBall`

ENNReal

Definitions

Name	Category	Theorems
`ltTopHomeomorphNNReal` 📖	CompOp	—
`neTopHomeomorphNNReal` 📖	CompOp	—
`truncateToReal` 📖	CompOp	5 math math: `truncateToReal_le`, `monotone_truncateToReal`, `continuous_truncateToReal`, `truncateToReal_eq_toReal`, `truncateToReal_nonneg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_mem_nhds` 📖	mathematical	—	`Set` `ENNReal` `Filter` `Filter.instMembership` `nhds` `instTopologicalSpace` `Set.Icc` `PartialOrder.toPreorder` `instPartialOrder` `instSub` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`Filter.HasBasis.mem_of_mem` `hasBasis_nhds_of_ne_top'`
`biInf_le_nhds` 📖	mathematical	—	`Filter` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `iInf` `Filter.instInfSet` `Preorder.toLT` `instPartialOrder` `instZeroENNReal` `Filter.principal` `Set.Icc` `instSub` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `nhds` `instTopologicalSpace`	—	`iInf₂_le_of_le` `one_pos` `IsOrderedRing.toZeroLEOneClass` `instIsOrderedRing` `NeZero.one` `top_add` `Set.Icc_self` `Filter.principal_singleton` `pure_le_nhds` `Eq.ge` `nhds_of_ne_top` `coe_ne_top`
`coe_range_mem_nhds` 📖	mathematical	—	`Set` `ENNReal` `Filter` `Filter.instMembership` `nhds` `instTopologicalSpace` `ofNNReal` `Set.range` `NNReal`	—	`IsOpen.mem_nhds` `Topology.IsOpenEmbedding.isOpen_range` `isOpenEmbedding_coe` `Set.mem_range_self`
`continuousAt_coe_iff` 📖	mathematical	—	`ContinuousAt` `ENNReal` `instTopologicalSpace` `ofNNReal` `NNReal` `NNReal.instTopologicalSpace`	—	`tendsto_nhds_coe_iff`
`continuousAt_const_mul` 📖	mathematical	—	`ContinuousAt` `ENNReal` `instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`Tendsto.const_mul` `Filter.tendsto_id`
`continuousAt_mul_const` 📖	mathematical	—	`ContinuousAt` `ENNReal` `instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`Tendsto.mul_const` `Filter.tendsto_id`
`continuousAt_toReal` 📖	mathematical	—	`ContinuousAt` `ENNReal` `Real` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `toReal`	—	`ContinuousOn.continuousAt` `continuousOn_toReal` `IsOpen.mem_nhds_iff` `isOpen_ne_top`
`continuousOn_sub` 📖	mathematical	—	`ContinuousOn` `ENNReal` `instTopologicalSpaceProd` `instTopologicalSpace` `instSub` `setOf` `Top.top` `instTopENNReal`	—	`ContinuousOn.eq_1` `tendsto_nhdsWithin_of_tendsto_nhds` `tendsto_sub` `not_and_or`
`continuousOn_sub_left` 📖	mathematical	—	`ContinuousOn` `ENNReal` `instTopologicalSpace` `instSub` `setOf` `Top.top` `instTopENNReal`	—	`ContinuousOn.comp` `continuousOn_sub` `ContinuousOn.prodMk` `continuousOn_const` `continuousOn_id'` `none_eq_top`
`continuousOn_toNNReal` 📖	mathematical	—	`ContinuousOn` `ENNReal` `NNReal` `instTopologicalSpace` `NNReal.instTopologicalSpace` `toNNReal` `setOf` `Top.top` `instTopENNReal`	—	`ContinuousAt.continuousWithinAt` `tendsto_toNNReal`
`continuousOn_toReal` 📖	mathematical	—	`ContinuousOn` `ENNReal` `Real` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `toReal` `setOf` `Top.top` `instTopENNReal`	—	`Continuous.comp_continuousOn` `NNReal.continuous_coe` `continuousOn_toNNReal`
`continuous_coe` 📖	mathematical	—	`Continuous` `NNReal` `ENNReal` `NNReal.instTopologicalSpace` `instTopologicalSpace` `ofNNReal`	—	`Topology.IsEmbedding.continuous` `isEmbedding_coe`
`continuous_coe_iff` 📖	mathematical	—	`Continuous` `ENNReal` `instTopologicalSpace` `ofNNReal` `NNReal` `NNReal.instTopologicalSpace`	—	`Topology.IsEmbedding.continuous_iff` `isEmbedding_coe`
`continuous_const_mul` 📖	mathematical	—	`Continuous` `ENNReal` `instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`continuous_iff_continuousAt` `continuousAt_const_mul`
`continuous_div_const` 📖	mathematical	—	`Continuous` `ENNReal` `instTopologicalSpace` `DivInvMonoid.toDiv` `instDivInvMonoid`	—	`continuous_mul_const` `inv_ne_top`
`continuous_mul_const` 📖	mathematical	—	`Continuous` `ENNReal` `instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`continuous_iff_continuousAt` `continuousAt_mul_const`
`continuous_nnreal_sub` 📖	mathematical	—	`Continuous` `ENNReal` `instTopologicalSpace` `instSub` `ofNNReal`	—	`continuous_sub_left` `coe_ne_top`
`continuous_ofReal` 📖	mathematical	—	`Continuous` `Real` `ENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instTopologicalSpace` `ofReal`	—	`Continuous.comp` `continuous_coe_iff` `continuous_id` `continuous_real_toNNReal`
`continuous_pow` 📖	mathematical	—	`Continuous` `ENNReal` `instTopologicalSpace` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `instCommSemiring`	—	`pow_zero` `pow_add` `pow_one` `Tendsto.mul` `Continuous.tendsto` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors` `instNoZeroDivisors` `Filter.tendsto_id`
`continuous_sub_left` 📖	mathematical	—	`Continuous` `ENNReal` `instTopologicalSpace` `instSub`	—	`ContinuousOn.comp_continuous` `continuousOn_sub` `Continuous.prodMk_right`
`continuous_sub_right` 📖	mathematical	—	`Continuous` `ENNReal` `instTopologicalSpace` `instSub`	—	`tsub_eq_zero_of_le` `instCanonicallyOrderedAdd` `instOrderedSub` `ContinuousOn.comp_continuous` `continuousOn_sub` `Continuous.prodMk` `continuous_id'` `continuous_const`
`continuous_truncateToReal` 📖	mathematical	—	`Continuous` `ENNReal` `Real` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `truncateToReal`	—	`ContinuousOn.comp_continuous` `continuousOn_toReal` `Continuous.min` `OrderTopology.to_orderClosedTopology` `instOrderTopology` `continuous_const` `continuous_id'`
`continuous_zpow` 📖	mathematical	—	`Continuous` `ENNReal` `instTopologicalSpace` `DivInvMonoid.toZPow` `instDivInvMonoid`	—	`zpow_natCast` `continuous_pow` `zpow_negSucc` `Continuous.inv` `instContinuousInv`
`eventuallyEq_of_toReal_eventuallyEq` 📖	mathematical	`Filter.Eventually` `ENNReal` `Top.top` `instTopENNReal` `Filter.EventuallyEq` `Real` `toReal`	`Filter.EventuallyEq` `ENNReal`	—	`Filter.mp_mem` `Filter.univ_mem'` `toReal_eq_toReal_iff'`
`exists_countable_dense_no_zero_top` 📖	mathematical	—	`Set` `ENNReal` `Set.Countable` `Dense` `instTopologicalSpace` `Set.instMembership` `instZeroENNReal` `Top.top` `instTopENNReal`	—	`exists_countable_dense_no_bot_top` `instOrderTopology` `instDenselyOrdered` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopology` `bot_eq_zero'` `instCanonicallyOrderedAdd`
`exists_frequently_lt_of_liminf_ne_top` 📖	mathematical	—	`Real` `Filter.Frequently` `Real.instLT`	—	`eq_top_of_forall_nnreal_le` `Filter.le_limsInf_of_le` `Filter.isCobounded_ge_of_top` `Filter.mp_mem` `Filter.univ_mem'` `LE.le.trans` `le_abs_self`
`exists_frequently_lt_of_liminf_ne_top'` 📖	mathematical	—	`Real` `Filter.Frequently` `Real.instLT`	—	`eq_top_of_forall_nnreal_le` `Filter.le_limsInf_of_le` `Filter.isCobounded_ge_of_top` `Filter.mp_mem` `Filter.univ_mem'` `LE.le.trans` `le_neg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `neg_le_abs`
`exists_upcrossings_of_not_bounded_under` 📖	mathematical	`Filter.IsBoundedUnder` `Real` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup`	`Filter.Frequently` `Real` `Real.instLT` `Real.instRatCast`	—	`not_and_or` `Filter.isBoundedUnder_le_abs` `Real.instIsOrderedAddMonoid` `exists_frequently_lt_of_liminf_ne_top` `exists_rat_gt` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `lt_add_iff_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Rat.instIsStrictOrderedRing` `Rat.instAddLeftMono` `contravariant_lt_of_covariant_le` `zero_lt_one` `Rat.instZeroLEOneClass` `NeZero.one` `Rat.nontrivial` `Filter.mp_mem` `Filter.univ_mem'` `not_lt` `LT.lt.le` `lt_of_lt_of_le` `exists_frequently_lt_of_liminf_ne_top'` `exists_rat_lt` `sub_lt_self_iff` `LE.le.trans`
`hasBasis_nhds_of_ne_top` 📖	mathematical	—	`Filter.HasBasis` `ENNReal` `nhds` `instTopologicalSpace` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `instZeroENNReal` `Set.Icc` `instSub` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`instCanonicallyOrderedAdd` `hasBasis_nhds_of_ne_top'`
`hasBasis_nhds_of_ne_top'` 📖	mathematical	—	`Filter.HasBasis` `ENNReal` `nhds` `instTopologicalSpace` `instZeroENNReal` `Set.Icc` `PartialOrder.toPreorder` `instPartialOrder` `instSub` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`LE.le.eq_or_lt` `zero_le` `instCanonicallyOrderedAdd` `zero_tsub` `instOrderedSub` `zero_add` `Set.Icc_bot` `nhds_bot_basis_Iic` `instOrderTopology` `instDenselyOrdered` `Filter.HasBasis.to_hasBasis` `nhds_basis_Ioo'` `Ne.lt_top` `exists_between` `tsub_pos_of_lt` `lt_iff_exists_add_pos_lt` `LT.lt.ne'` `lt_min` `coe_pos` `Set.Icc_subset_Ioo` `lt_tsub_comm` `LE.le.trans_lt` `min_le_left` `lt_imp_lt_of_le_of_le` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `min_le_right` `le_refl` `sub_lt_self` `lt_add_right` `Set.Ioo_subset_Icc_self`
`inv_liminf` 📖	mathematical	—	`ENNReal` `instInv` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `Filter.limsup`	—	`OrderIso.liminf_apply` `Filter.isBounded_ge_of_bot` `Filter.isCobounded_ge_of_top`
`inv_limsup` 📖	mathematical	—	`ENNReal` `instInv` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `Filter.liminf`	—	`OrderIso.limsup_apply` `Filter.isBounded_le_of_top` `Filter.isCobounded_le_of_bot`
`isOpen_Ico_zero` 📖	mathematical	—	`IsOpen` `ENNReal` `instTopologicalSpace` `Set.Ico` `PartialOrder.toPreorder` `instPartialOrder` `instZeroENNReal`	—	`Ico_eq_Iio` `isOpen_Iio` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopology`
`isOpen_ne_top` 📖	mathematical	—	`IsOpen` `ENNReal` `instTopologicalSpace` `setOf` `Top.top` `instTopENNReal`	—	`isOpen_ne` `T5Space.toT1Space` `instT5Space`
`le_liminf_mul` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `Pi.instMul`	—	`mul_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` `mul_lt_mul`
`le_limsup_mul` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `Filter.liminf` `Pi.instMul`	—	`mul_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` `mul_lt_mul`
`le_of_forall_lt_one_mul_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`Filter.Tendsto.mono_left` `continuousAt_mul_const` `one_ne_zero` `NeZero.one` `inf_le_left` `le_of_tendsto` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopology` `nhdsLT_neBot` `one_mul` `eventually_nhdsWithin_iff` `Filter.Eventually.of_forall`
`liminf_add_of_left_tendsto_zero` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `instTopologicalSpace` `instZeroENNReal`	`Filter.liminf` `ENNReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`add_comm` `liminf_add_of_right_tendsto_zero`
`liminf_add_of_right_tendsto_zero` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `instTopologicalSpace` `instZeroENNReal`	`Filter.liminf` `ENNReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`le_antisymm` `Filter.liminf_le_of_le` `Filter.isBounded_ge_of_bot` `Filter.le_liminf_iff'` `instDenselyOrdered` `Filter.isCobounded_ge_of_top` `Filter.mp_mem` `tendsto_nhds_zero` `lt_min` `tsub_pos_of_lt` `instCanonicallyOrderedAdd` `instOrderedSub` `one_pos` `IsOrderedRing.toZeroLEOneClass` `instIsOrderedRing` `NeZero.one` `Filter.univ_mem'` `le_of_add_le_add_right` `LT.lt.ne` `LE.le.trans_lt` `LE.le.trans` `add_le_of_le_tsub_left_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `LT.lt.le` `min_le_left` `Filter.liminf_le_liminf` `Filter.Eventually.of_forall`
`liminf_const_sub` 📖	mathematical	—	`Filter.liminf` `ENNReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `instSub` `Filter.limsup`	—	`Antitone.map_limsSup_of_continuousAt` `instOrderTopology` `Filter.map_neBot` `tsub_le_tsub_left` `instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Continuous.continuousAt` `continuous_sub_left` `Filter.isBounded_le_of_top` `Filter.isCobounded_le_of_bot`
`liminf_mul_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `Filter.limsup`	—	`le_mul_of_forall_lt` `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` `mul_lt_mul`
`liminf_sub_const` 📖	mathematical	—	`Filter.liminf` `ENNReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `instSub`	—	`Monotone.map_limsInf_of_continuousAt` `instOrderTopology` `Filter.map_neBot` `tsub_le_tsub_right` `instOrderedSub` `Continuous.continuousAt` `continuous_sub_right` `Filter.isCobounded_ge_of_top` `Filter.isBounded_ge_of_bot`
`liminf_toReal_eq` 📖	mathematical	`Filter.Eventually` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Filter.liminf` `Real` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Real.instConditionallyCompleteLinearOrder` `toReal` `ENNReal` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder`	—	`Filter.liminf_le_of_le` `instCanonicallyOrderedAdd` `Filter.Eventually.exists` `Filter.Eventually.and` `LE.le.trans` `Filter.mp_mem` `Filter.univ_mem'` `truncateToReal_eq_toReal` `Filter.liminf_congr` `Monotone.map_liminf_of_continuousAt` `instOrderTopology` `instOrderTopologyReal` `monotone_truncateToReal` `Continuous.continuousAt` `continuous_truncateToReal` `Filter.IsBoundedUnder.isCoboundedUnder_ge` `Filter.Eventually.of_forall`
`limsup_add_of_left_tendsto_zero` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `instTopologicalSpace` `instZeroENNReal`	`Filter.limsup` `ENNReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`add_comm` `limsup_add_of_right_tendsto_zero`
`limsup_add_of_right_tendsto_zero` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `instTopologicalSpace` `instZeroENNReal`	`Filter.limsup` `ENNReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`le_antisymm` `Filter.le_limsup_of_le` `Filter.isBounded_le_of_top` `Filter.limsup_le_iff'` `instDenselyOrdered` `Filter.isCobounded_le_of_bot` `Filter.mp_mem` `tendsto_nhds_zero` `tsub_pos_of_lt` `instCanonicallyOrderedAdd` `instOrderedSub` `Filter.univ_mem'` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `add_le_of_le_tsub_left_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `LT.lt.le` `Filter.limsup_le_limsup` `Filter.Eventually.of_forall`
`limsup_const_sub` 📖	mathematical	—	`Filter.limsup` `ENNReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `instSub` `Filter.liminf`	—	`Filter.eq_or_neBot` `Filter.limsup_bot` `bot_eq_zero'` `instCanonicallyOrderedAdd` `Filter.liminf_bot` `sub_top` `Antitone.map_limsInf_of_continuousAt` `instOrderTopology` `Filter.map_neBot` `tsub_le_tsub_left` `instOrderedSub` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Continuous.continuousAt` `continuous_sub_left` `Filter.isCobounded_ge_of_top` `Filter.isBounded_ge_of_bot`
`limsup_mul_le'` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`le_mul_of_forall_lt` `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` `mul_lt_mul`
`limsup_sub_const` 📖	mathematical	—	`Filter.limsup` `ENNReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder` `instSub`	—	`Filter.eq_or_neBot` `Filter.limsup_bot` `bot_eq_zero'` `instCanonicallyOrderedAdd` `zero_tsub` `instOrderedSub` `Monotone.map_limsSup_of_continuousAt` `instOrderTopology` `Filter.map_neBot` `tsub_le_tsub_right` `Continuous.continuousAt` `continuous_sub_right` `Filter.isBounded_le_of_top` `Filter.isCobounded_le_of_bot`
`limsup_toReal_eq` 📖	mathematical	`Filter.Eventually` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Filter.limsup` `Real` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Real.instConditionallyCompleteLinearOrder` `toReal` `ENNReal` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder`	—	`Filter.mp_mem` `Filter.univ_mem'` `truncateToReal_eq_toReal` `Filter.limsup_le_of_le` `instCanonicallyOrderedAdd` `Filter.limsup_congr` `Monotone.map_limsup_of_continuousAt` `instOrderTopology` `instOrderTopologyReal` `monotone_truncateToReal` `Continuous.continuousAt` `continuous_truncateToReal` `Filter.IsBoundedUnder.isCoboundedUnder_le` `Filter.Eventually.of_forall`
`monotone_truncateToReal` 📖	mathematical	—	`Monotone` `ENNReal` `Real` `PartialOrder.toPreorder` `instPartialOrder` `Real.instPreorder` `truncateToReal`	—	`toReal_mono` `ne_top_of_le_ne_top` `min_le_left` `inf_le_inf` `le_refl`
`nhdsGT_coe_neBot` 📖	mathematical	—	`Filter.NeBot` `ENNReal` `nhdsWithin` `instTopologicalSpace` `ofNNReal` `Set.Ioi` `PartialOrder.toPreorder` `instPartialOrder`	—	`nhdsGT_neBot_of_exists_gt` `instOrderTopology` `instDenselyOrdered` `coe_lt_top`
`nhdsGT_nat_neBot` 📖	mathematical	—	`Filter.NeBot` `ENNReal` `nhdsWithin` `instTopologicalSpace` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Set.Ioi` `PartialOrder.toPreorder` `instPartialOrder`	—	`nhdsGT_coe_neBot`
`nhdsGT_ofNat_neBot` 📖	mathematical	—	`Filter.NeBot` `ENNReal` `nhdsWithin` `instTopologicalSpace` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Set.Ioi` `PartialOrder.toPreorder` `instPartialOrder`	—	`nhdsGT_coe_neBot`
`nhdsGT_one_neBot` 📖	mathematical	—	`Filter.NeBot` `ENNReal` `nhdsWithin` `instTopologicalSpace` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Set.Ioi` `PartialOrder.toPreorder` `instPartialOrder`	—	`nhdsGT_coe_neBot`
`nhdsGT_zero_neBot` 📖	mathematical	—	`Filter.NeBot` `ENNReal` `nhdsWithin` `instTopologicalSpace` `instZeroENNReal` `Set.Ioi` `PartialOrder.toPreorder` `instPartialOrder`	—	`nhdsGT_coe_neBot`
`nhdsLT_neBot` 📖	mathematical	—	`Filter.NeBot` `ENNReal` `nhdsWithin` `instTopologicalSpace` `Set.Iio` `PartialOrder.toPreorder` `instPartialOrder`	—	`nhdsLT_neBot_of_exists_lt` `instOrderTopology` `instDenselyOrdered` `NeZero.pos` `instCanonicallyOrderedAdd`
`nhds_coe` 📖	mathematical	—	`nhds` `ENNReal` `instTopologicalSpace` `ofNNReal` `Filter.map` `NNReal` `NNReal.instTopologicalSpace`	—	`Topology.IsOpenEmbedding.map_nhds_eq` `isOpenEmbedding_coe`
`nhds_of_ne_top` 📖	mathematical	—	`nhds` `ENNReal` `instTopologicalSpace` `iInf` `Filter` `Filter.instInfSet` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `instZeroENNReal` `Filter.principal` `Set.Icc` `instSub` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`Filter.HasBasis.eq_biInf` `hasBasis_nhds_of_ne_top`
`nhds_top` 📖	mathematical	—	`nhds` `ENNReal` `instTopologicalSpace` `Top.top` `instTopENNReal` `iInf` `Filter` `Filter.instInfSet` `Filter.principal` `Set.Ioi` `PartialOrder.toPreorder` `instPartialOrder`	—	`nhds_top_order` `instOrderTopology` `iInf_congr_Prop`
`nhds_top'` 📖	mathematical	—	`nhds` `ENNReal` `instTopologicalSpace` `Top.top` `instTopENNReal` `iInf` `Filter` `NNReal` `Filter.instInfSet` `Filter.principal` `Set.Ioi` `PartialOrder.toPreorder` `instPartialOrder` `ofNNReal`	—	`nhds_top` `iInf_ne_top`
`nhds_top_basis` 📖	mathematical	—	`Filter.HasBasis` `ENNReal` `nhds` `instTopologicalSpace` `Top.top` `instTopENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Set.Ioi`	—	`nhds_top_basis` `instOrderTopology`
`nhds_zero` 📖	mathematical	—	`nhds` `ENNReal` `instTopologicalSpace` `instZeroENNReal` `iInf` `Filter` `Filter.instInfSet` `Filter.principal` `Set.Iio` `PartialOrder.toPreorder` `instPartialOrder`	—	`nhds_bot_order` `instOrderTopology` `iInf_congr_Prop` `bot_eq_zero'` `instCanonicallyOrderedAdd`
`nhds_zero_basis` 📖	mathematical	—	`Filter.HasBasis` `ENNReal` `nhds` `instTopologicalSpace` `instZeroENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Set.Iio`	—	`nhds_bot_basis` `instOrderTopology`
`nhds_zero_basis_Iic` 📖	mathematical	—	`Filter.HasBasis` `ENNReal` `nhds` `instTopologicalSpace` `instZeroENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Set.Iic`	—	`nhds_bot_basis_Iic` `instOrderTopology` `instDenselyOrdered`
`ofNNReal_liminf` 📖	mathematical	`Filter.IsCoboundedUnder` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder`	`ofNNReal` `Filter.liminf` `NNReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `NNReal.instConditionallyCompleteLinearOrderBot` `ENNReal` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder`	—	`eq_of_forall_nnreal_le_iff` `coe_le_coe` `Filter.le_liminf_iff` `Filter.isBounded_ge_of_bot` `Filter.isCobounded_ge_of_top` `instIsEmptyFalse`
`ofNNReal_limsup` 📖	mathematical	`Filter.IsBoundedUnder` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder`	`ofNNReal` `Filter.limsup` `NNReal` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `NNReal.instConditionallyCompleteLinearOrderBot` `ENNReal` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrder`	—	`eq_of_forall_nnreal_le_iff` `coe_le_coe` `Filter.le_limsup_iff` `Filter.isCobounded_le_of_bot` `Filter.isBounded_le_of_top`
`tendsto_atTop` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `nhds` `instTopologicalSpace` `Set` `Set.instMembership` `Set.Icc` `instPartialOrder` `instSub` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`Filter.HasBasis.tendsto_iff` `Filter.atTop_basis` `SemilatticeSup.instIsDirectedOrder` `hasBasis_nhds_of_ne_top`
`tendsto_atTop_zero` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `nhds` `instTopologicalSpace` `instZeroENNReal` `Preorder.toLE` `instPartialOrder`	—	`Filter.HasBasis.tendsto_iff` `Filter.atTop_basis` `SemilatticeSup.instIsDirectedOrder` `nhds_zero_basis_Iic`
`tendsto_atTop_zero_iff_le_of_antitone` 📖	mathematical	`Antitone` `ENNReal` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instPartialOrder`	`Filter.Tendsto` `ENNReal` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `nhds` `instTopologicalSpace` `instZeroENNReal` `Preorder.toLE` `instPartialOrder`	—	`tendsto_atTop_zero` `le_rfl` `LE.le.trans`
`tendsto_atTop_zero_iff_lt_of_antitone` 📖	mathematical	`Antitone` `ENNReal` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instPartialOrder`	`Filter.Tendsto` `ENNReal` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `nhds` `instTopologicalSpace` `instZeroENNReal` `Preorder.toLT` `instPartialOrder`	—	`tendsto_atTop_zero_iff_le_of_antitone` `Nat.instAtLeastTwoHAddOfNat` `lt_min_iff` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `instIsOrderedRing` `NeZero.one` `div_pos_iff` `ne_of_gt` `ofNat_ne_top` `LE.le.trans_lt` `min_le_left` `one_lt_top` `min_le_right` `div_lt_iff` `LT.lt.ne'` `mul_one` `mul_lt_mul_right` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instCharZero` `LT.lt.le`
`tendsto_coe_nhds_top` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `ofNNReal` `nhds` `instTopologicalSpace` `Top.top` `instTopENNReal` `NNReal` `Filter.atTop` `PartialOrder.toPreorder` `NNReal.instPartialOrder`	—	`tendsto_nhds_top_iff_nnreal` `Filter.HasBasis.tendsto_right_iff` `Filter.atTop_basis_Ioi` `instIsDirectedOrder` `IsStrictOrderedRing.toNoMaxOrder`
`tendsto_coe_sub` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `instSub` `ofNNReal` `nhds` `instTopologicalSpace`	—	`Continuous.tendsto` `continuous_nnreal_sub`
`tendsto_coe_toNNReal` 📖	mathematical	—	`Filter.Tendsto` `NNReal` `ENNReal` `ofNNReal` `nhds` `NNReal.instTopologicalSpace` `toNNReal` `instTopologicalSpace`	—	`coe_toNNReal` `Continuous.tendsto` `continuous_coe`
`tendsto_const_sub_nhds_zero_iff` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Filter.Tendsto` `ENNReal` `instSub` `nhds` `instTopologicalSpace` `instZeroENNReal`	—	`tendsto_nhds_zero` `tendsto_nhds` `Filter.mp_mem` `Filter.univ_mem'` `tsub_le_iff_right` `instOrderedSub` `add_comm` `LE.le.trans` `le_add_right` `instCanonicallyOrderedAdd` `le_rfl`
`tendsto_finset_prod_of_ne_top` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `instTopologicalSpace`	`Filter.Tendsto` `ENNReal` `Finset.prod` `CommSemiring.toCommMonoid` `instCommSemiring` `nhds` `instTopologicalSpace`	—	`Finset.induction` `Finset.prod_insert` `Tendsto.mul` `Finset.mem_insert_self` `prod_ne_top` `Finset.mem_insert_of_mem`
`tendsto_inv_iff` 📖	mathematical	—	`Filter.Tendsto` `InvolutiveInv.toInv` `nhds`	—	`tendsto_inv_iff`
`tendsto_inv_nat_nhds_zero` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `instInv` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Filter.atTop` `Nat.instPreorder` `nhds` `instTopologicalSpace` `instZeroENNReal`	—	`tendsto_inv_iff` `instContinuousInv` `tendsto_nat_nhds_top` `inv_top`
`tendsto_mul` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `nhds` `instTopologicalSpaceProd` `instTopologicalSpace`	—	`tendsto_nhds_top_iff_nnreal` `lt_iff_exists_nnreal_btwn` `pos_iff_ne_zero` `instCanonicallyOrderedAdd` `Filter.Eventually.prod_nhds` `lt_mem_nhds` `instOrderTopology` `div_lt_top` `coe_ne_top` `LT.lt.ne'` `Filter.Eventually.mono` `Eq.trans_lt` `div_mul_cancel` `mul_lt_mul` `top_mul` `mul_top` `mul_comm` `Filter.Tendsto.comp` `Continuous.tendsto` `continuous_swap` `nhds_coe_coe` `IsTopologicalSemiring.toContinuousMul` `NNReal.instIsTopologicalSemiring`
`tendsto_nat_nhds_top` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Filter.atTop` `Nat.instPreorder` `nhds` `instTopologicalSpace` `Top.top` `instTopENNReal`	—	`tendsto_nhds_top` `Filter.mem_atTop_sets` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Set.mem_setOf` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `instIsOrderedRing` `instCharZero`
`tendsto_nhds` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `nhds` `instTopologicalSpace` `Filter.Eventually` `Set` `Set.instMembership` `Set.Icc` `PartialOrder.toPreorder` `instPartialOrder` `instSub` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`nhds_of_ne_top`
`tendsto_nhds_coe_iff` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `nhds` `instTopologicalSpace` `ofNNReal` `NNReal` `NNReal.instTopologicalSpace`	—	`nhds_coe` `Filter.tendsto_map'_iff`
`tendsto_nhds_of_Icc` 📖	mathematical	`Filter.Eventually` `ENNReal` `Set` `Set.instMembership` `Set.Icc` `PartialOrder.toPreorder` `instPartialOrder` `instSub` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	`Filter.Tendsto` `ENNReal` `nhds` `instTopologicalSpace`	—	`Filter.Tendsto.mono_right` `biInf_le_nhds`
`tendsto_nhds_top` 📖	mathematical	`Filter.Eventually` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Filter.Tendsto` `ENNReal` `nhds` `instTopologicalSpace` `Top.top` `instTopENNReal`	—	`tendsto_nhds_top_iff_nat`
`tendsto_nhds_top_iff_nat` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `nhds` `instTopologicalSpace` `Top.top` `instTopENNReal` `Filter.Eventually` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`tendsto_nhds_top_iff_nnreal` `exists_nat_gt` `Filter.Eventually.mono` `lt_trans` `coe_natCast` `coe_lt_coe`
`tendsto_nhds_top_iff_nnreal` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `nhds` `instTopologicalSpace` `Top.top` `instTopENNReal` `Filter.Eventually` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `ofNNReal`	—	`nhds_top'`
`tendsto_nhds_zero` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `nhds` `instTopologicalSpace` `instZeroENNReal` `Filter.Eventually` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`Filter.HasBasis.tendsto_right_iff` `nhds_zero_basis_Iic`
`tendsto_ofReal` 📖	mathematical	`Filter.Tendsto` `Real` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Filter.Tendsto` `ENNReal` `ofReal` `nhds` `instTopologicalSpace`	—	`Filter.Tendsto.comp` `Continuous.tendsto` `continuous_ofReal`
`tendsto_ofReal_atTop` 📖	mathematical	—	`Filter.Tendsto` `Real` `ENNReal` `ofReal` `Filter.atTop` `Real.instPreorder` `nhds` `instTopologicalSpace` `Top.top` `instTopENNReal`	—	`tendsto_ofReal_nhds_top` `Filter.tendsto_id`
`tendsto_ofReal_nhds_top` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `ofReal` `nhds` `instTopologicalSpace` `Top.top` `instTopENNReal` `Real` `Filter.atTop` `Real.instPreorder`	—	`tendsto_coe_nhds_top` `Real.tendsto_toNNReal_atTop_iff`
`tendsto_sub` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `instSub` `nhds` `instTopologicalSpaceProd` `instTopologicalSpace`	—	`top_sub_coe` `tendsto_nhds_top_iff_nnreal` `Filter.Eventually.mono` `Filter.Eventually.prod_nhds` `lt_mem_nhds` `instOrderTopology` `coe_lt_top` `ge_mem_nhds` `coe_lt_coe` `lt_add_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.one` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `NNReal.addLeftMono` `lt_tsub_iff_left` `instOrderedSub` `lt_imp_lt_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `le_refl` `sub_top` `Filter.Tendsto.mono_right` `Filter.tendsto_pure` `gt_mem_nhds` `tsub_eq_zero_iff_le` `instCanonicallyOrderedAdd` `LT.lt.le` `LT.lt.trans` `pure_le_nhds` `nhds_coe_coe` `Continuous.tendsto` `ContinuousSub.continuous_sub` `NNReal.instContinuousSub`
`tendsto_toNNReal` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `NNReal` `toNNReal` `nhds` `instTopologicalSpace` `NNReal.instTopologicalSpace`	—	`CanLift.prf` `canLift` `nhds_coe` `Filter.tendsto_map'_iff` `Filter.tendsto_id`
`tendsto_toNNReal_iff` 📖	mathematical	—	`Filter.Tendsto` `NNReal` `ENNReal` `toNNReal` `nhds` `NNReal.instTopologicalSpace` `instTopologicalSpace`	—	`coe_comp_toNNReal_comp` `Filter.Tendsto.comp` `tendsto_coe_toNNReal` `tendsto_toNNReal`
`tendsto_toNNReal_iff'` 📖	mathematical	—	`Filter.Tendsto` `NNReal` `ENNReal` `toNNReal` `nhds` `NNReal.instTopologicalSpace` `instTopologicalSpace` `ofNNReal`	—	`toNNReal_coe` `tendsto_toNNReal_iff` `coe_ne_top`
`tendsto_toReal` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `Real` `toReal` `nhds` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`NNReal.tendsto_coe` `tendsto_toNNReal`
`tendsto_toReal_iff` 📖	mathematical	—	`Filter.Tendsto` `Real` `toReal` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ENNReal` `instTopologicalSpace`	—	`CanLift.prf` `Pi.canLift` `canLift`
`tendsto_toReal_zero_iff` 📖	mathematical	—	`Filter.Tendsto` `Real` `toReal` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `ENNReal` `instTopologicalSpace` `instZeroENNReal`	—	`toReal_zero` `tendsto_toReal_iff` `zero_ne_top`
`truncateToReal_eq_toReal` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`truncateToReal` `toReal`	—	`lt_of_le_of_lt` `Ne.lt_top` `toReal_eq_toReal_iff'` `LT.lt.ne` `min_eq_right`
`truncateToReal_le` 📖	mathematical	—	`Real` `Real.instLE` `truncateToReal` `toReal`	—	`truncateToReal.eq_1` `toReal_mono` `min_le_left`
`truncateToReal_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `truncateToReal`	—	`toReal_nonneg`

ENNReal.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`const_div` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `ENNReal.instTopologicalSpace`	`Filter.Tendsto` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `nhds` `ENNReal.instTopologicalSpace`	—	`const_mul` `tendsto_inv_iff` `ENNReal.instContinuousInv`
`const_mul` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `ENNReal.instTopologicalSpace`	`Filter.Tendsto` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `nhds` `ENNReal.instTopologicalSpace`	—	`by_cases` `MulZeroClass.zero_mul` `mul` `tendsto_const_nhds`
`div` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `ENNReal.instTopologicalSpace`	`Filter.Tendsto` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `nhds` `ENNReal.instTopologicalSpace`	—	`mul` `tendsto_inv_iff` `ENNReal.instContinuousInv`
`div_const` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `ENNReal.instTopologicalSpace`	`Filter.Tendsto` `ENNReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `nhds` `ENNReal.instTopologicalSpace`	—	`mul_const`
`mul` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `ENNReal.instTopologicalSpace`	`Filter.Tendsto` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `nhds` `ENNReal.instTopologicalSpace`	—	`Filter.Tendsto.comp` `ENNReal.tendsto_mul` `Filter.Tendsto.prodMk_nhds`
`mul_const` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `ENNReal.instTopologicalSpace`	`Filter.Tendsto` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `nhds` `ENNReal.instTopologicalSpace`	—	`mul_comm` `const_mul`
`pow` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `ENNReal.instTopologicalSpace`	`Filter.Tendsto` `ENNReal` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `nhds` `ENNReal.instTopologicalSpace`	—	`Filter.Tendsto.comp` `Continuous.tendsto` `ENNReal.continuous_pow`
`sub` 📖	mathematical	`Filter.Tendsto` `ENNReal` `nhds` `ENNReal.instTopologicalSpace`	`Filter.Tendsto` `ENNReal` `ENNReal.instSub` `nhds` `ENNReal.instTopologicalSpace`	—	`Filter.Tendsto.comp` `ENNReal.tendsto_sub` `Filter.Tendsto.prodMk_nhds`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edist` 📖	mathematical	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Filter.Tendsto` `ENNReal` `EDist.edist` `PseudoEMetricSpace.toEDist` `nhds` `ENNReal.instTopologicalSpace`	—	`comp` `Continuous.tendsto` `continuous_edist` `prodMk_nhds`

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `closure` `LipschitzOnWith`	`LipschitzOnWith` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`ENNReal.continuous_const_mul` `ENNReal.coe_ne_top` `le_on_closure` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Continuous.comp_continuousOn'` `Continuous.edist` `continuous_id'` `continuous_const` `Continuous.continuousOn`

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diam_closure` 📖	mathematical	—	`diam` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`ediam_closure`
`ediam_closure` 📖	mathematical	—	`ediam` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`le_antisymm` `ediam_le` `map_mem_closure₂` `continuous_edist` `edist_le_ediam_of_mem` `closure_Iic` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `ediam_mono` `subset_closure`
`isClosed_closedEBall` 📖	mathematical	—	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `closedEBall`	—	`isClosed_le` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Continuous.edist` `continuous_id'` `continuous_const`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diam_Icc` 📖	mathematical	`Real` `instLE`	`Metric.diam` `Real` `pseudoMetricSpace` `Set.Icc` `instPreorder` `instSub`	—	`ediam_Icc` `ENNReal.toReal_ofReal` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`diam_Ico` 📖	mathematical	`Real` `instLE`	`Metric.diam` `Real` `pseudoMetricSpace` `Set.Ico` `instPreorder` `instSub`	—	`ediam_Ico` `ENNReal.toReal_ofReal` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`diam_Ioc` 📖	mathematical	`Real` `instLE`	`Metric.diam` `Real` `pseudoMetricSpace` `Set.Ioc` `instPreorder` `instSub`	—	`ediam_Ioc` `ENNReal.toReal_ofReal` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`diam_Ioo` 📖	mathematical	`Real` `instLE`	`Metric.diam` `Real` `pseudoMetricSpace` `Set.Ioo` `instPreorder` `instSub`	—	`ediam_Ioo` `ENNReal.toReal_ofReal` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`diam_eq` 📖	mathematical	`Bornology.IsBounded` `Real` `PseudoMetricSpace.toBornology` `pseudoMetricSpace`	`Metric.diam` `Real` `pseudoMetricSpace` `instSub` `SupSet.sSup` `instSupSet` `InfSet.sInf` `instInfSet`	—	`Metric.diam.eq_1` `ediam_eq` `ENNReal.toReal_ofReal` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `sInf_le_sSup` `Bornology.IsBounded.bddBelow` `instIsOrderBornology` `Bornology.IsBounded.bddAbove`
`ediam_Icc` 📖	mathematical	—	`Metric.ediam` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace` `Set.Icc` `instPreorder` `ENNReal.ofReal` `instSub`	—	`le_or_gt` `ediam_eq` `Metric.isBounded_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `csSup_Icc` `csInf_Icc` `Set.Icc_eq_empty` `Metric.ediam_empty` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `zero_add` `LT.lt.le`
`ediam_Ico` 📖	mathematical	—	`Metric.ediam` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace` `Set.Ico` `instPreorder` `ENNReal.ofReal` `instSub`	—	`le_antisymm` `Metric.ediam_mono` `Set.Ico_subset_Icc_self` `ediam_Icc` `Set.Ioo_subset_Ico_self` `ediam_Ioo`
`ediam_Ioc` 📖	mathematical	—	`Metric.ediam` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace` `Set.Ioc` `instPreorder` `ENNReal.ofReal` `instSub`	—	`le_antisymm` `Metric.ediam_mono` `Set.Ioc_subset_Icc_self` `ediam_Icc` `Set.Ioo_subset_Ioc_self` `ediam_Ioo`
`ediam_Ioo` 📖	mathematical	—	`Metric.ediam` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace` `Set.Ioo` `instPreorder` `ENNReal.ofReal` `instSub`	—	`le_or_gt` `Set.Ioo_eq_empty` `Metric.ediam_empty` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `zero_add` `ediam_eq` `Metric.isBounded_Ioo` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `csSup_Ioo` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `csInf_Ioo`
`ediam_eq` 📖	mathematical	`Bornology.IsBounded` `Real` `PseudoMetricSpace.toBornology` `pseudoMetricSpace`	`Metric.ediam` `Real` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace` `ENNReal.ofReal` `instSub` `SupSet.sSup` `instSupSet` `InfSet.sInf` `instInfSet`	—	`Set.eq_empty_or_nonempty` `Metric.ediam_empty` `sSup_empty` `sInf_empty` `sub_self` `ENNReal.ofReal_zero` `le_antisymm` `Metric.ediam_le_of_forall_dist_le` `dist_le_of_mem_Icc` `Bornology.IsBounded.subset_Icc_sInf_sSup` `instIsOrderBornology` `ENNReal.ofReal_le_of_le_toReal` `Metric.diam.eq_1` `Metric.diam_closure` `le_abs_self` `Metric.dist_le_diam_of_mem` `Bornology.IsBounded.closure` `csSup_mem_closure` `instOrderTopologyReal` `Bornology.IsBounded.bddAbove` `csInf_mem_closure` `Bornology.IsBounded.bddBelow`

(root)

Definitions

Name	Category	Theorems
`metricSpaceEMetricBall` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_edist` 📖	mathematical	—	`Continuous` `ENNReal` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `ENNReal.instTopologicalSpace` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`continuous_of_le_add_edist` `Nat.instAtLeastTwoHAddOfNat` `edist_triangle4` `PseudoEMetricSpace.edist_comm` `AddSemigroup.to_isAssociative` `AddCommMagma.to_isCommutative` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `add_le_add` `covariant_swap_add_of_covariant_add` `le_max_left` `le_max_right` `mul_two` `mul_comm`
`continuous_of_le_add_edist` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Distrib.toMul` `EDist.edist` `PseudoEMetricSpace.toEDist`	`Continuous` `ENNReal` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `ENNReal.instTopologicalSpace`	—	`continuous_iff_continuousAt` `ENNReal.tendsto_nhds_of_Icc` `ENNReal.exists_nnreal_pos_mul_lt` `LT.lt.ne'` `Filter.mp_mem` `Metric.closedEBall_mem_nhds` `ENNReal.coe_pos` `Filter.univ_mem'` `tsub_le_iff_right` `ENNReal.instOrderedSub` `LE.le.trans` `le_imp_le_of_le_of_le` `le_refl` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `LT.lt.le` `mul_comm` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `Metric.mem_closedEBall'` `Metric.mem_closedEBall`
`edist_ne_top_of_mem_ball` 📖	—	—	—	—	`ne_of_lt` `edist_triangle_left` `PseudoEMetricSpace.edist_comm` `ENNReal.add_lt_add` `le_top`
`isClosed_setOf_lipschitzOnWith` 📖	mathematical	—	`IsClosed` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `setOf` `LipschitzOnWith`	—	`Set.setOf_forall` `Set.iInter_congr_Prop` `isClosed_biInter` `isClosed_le` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Continuous.edist` `continuous_apply` `continuous_const`
`isClosed_setOf_lipschitzWith` 📖	mathematical	—	`IsClosed` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `setOf` `LipschitzWith`	—	—
`lipschitzOnWith_closure_iff` 📖	mathematical	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `closure`	`LipschitzOnWith` `closure` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`LipschitzOnWith.mono` `subset_closure` `LipschitzOnWith.closure`
`nhds_eq_nhds_emetric_ball` 📖	mathematical	`Set` `Set.instMembership` `Metric.eball` `EMetricSpace.toPseudoEMetricSpace`	`nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `Filter.map` `Set` `Set.instMembership` `Metric.eball` `instTopologicalSpaceSubtype`	—	`map_nhds_subtype_coe_eq_nhds` `IsOpen.mem_nhds` `Metric.isOpen_eball`
`tendsto_iff_edist_tendsto_0` 📖	mathematical	—	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `ENNReal` `EDist.edist` `PseudoEMetricSpace.toEDist` `ENNReal.instTopologicalSpace` `instZeroENNReal`	—	`Filter.HasBasis.tendsto_right_iff` `Metric.nhds_basis_eball` `tendsto_order` `ENNReal.instOrderTopology` `ENNReal.not_lt_zero`

---

← Back to Index