NegMulLog

📁 Source: Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean

Statistics

Metric	Count
Definitions negMulLog	1
Theorems mul_log, concaveOn_negMulLog, continuous_mul_log, continuous_negMulLog, convexOn_mul_log, deriv2_mul_log, deriv2_negMulLog, deriv_mul_log, deriv_mul_log_zero, deriv_negMulLog, differentiableAt_negMulLog, differentiableAt_negMulLog_iff, differentiableOn_mul_log, differentiableOn_negMulLog, hasDerivAt_mul_log, hasDerivAt_negMulLog, leftDeriv_mul_log, mul_log_nonneg, mul_log_nonpos, negMulLog_def, negMulLog_eq_neg, negMulLog_mul, negMulLog_nonneg, negMulLog_one, negMulLog_zero, not_DifferentiableAt_log_mul_zero, not_continuousAt_deriv_mul_log_zero, rightDeriv_mul_log, strictConcaveOn_negMulLog, strictConvexOn_mul_log, tendsto_deriv_mul_log_atTop, tendsto_rightDeriv_mul_log_atTop	32
Total	33

Real

Definitions

Name	Category	Theorems
negMulLog 📖	CompOp	17 math math: deriv_negMulLog, negMulLog_mul, continuous_negMulLog, negMulLog_nonneg, concaveOn_negMulLog, differentiableOn_negMulLog, binEntropy_eq_negMulLog_add_negMulLog_one_sub', negMulLog_one, negMulLog_eq_neg, negMulLog_def, differentiableAt_negMulLog, negMulLog_zero, strictConcaveOn_negMulLog, binEntropy_eq_negMulLog_add_negMulLog_one_sub, deriv2_negMulLog, differentiableAt_negMulLog_iff, hasDerivAt_negMulLog

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
concaveOn_negMulLog 📖	mathematical	—	ConcaveOn Real semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici instPreorder instZero negMulLog	—	StrictConcaveOn.concaveOn strictConcaveOn_negMulLog
continuous_mul_log 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul log	—	continuous_iff_continuousAt ne_or_eq ContinuousAt.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.continuousAt continuous_id' continuousAt_log ContinuousAt.eq_1 MulZeroClass.zero_mul mul_comm nhdsWithin_univ Set.ext Set.Iio_union_Ioi Set.union_singleton nhdsWithin_union nhdsWithin_singleton tendsto_log_mul_self_nhdsLT_zero rpow_one tendsto_log_mul_rpow_nhdsGT_zero zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike log_zero MulZeroClass.mul_zero tendsto_pure_nhds
continuous_negMulLog 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace negMulLog	—	negMulLog_eq_neg Continuous.neg IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal continuous_mul_log
convexOn_mul_log 📖	mathematical	—	ConvexOn Real semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici instPreorder instZero instMul log	—	StrictConvexOn.convexOn strictConvexOn_mul_log
deriv2_mul_log 📖	mathematical	—	Nat.iterate deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul log instInv	—	inv_zero deriv_zero_of_not_differentiableAt not_continuousAt_deriv_mul_log_zero DifferentiableAt.continuousAt IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Filter.mp_mem eventually_ne_nhds T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal Filter.univ_mem' deriv_mul_log Filter.EventuallyEq.deriv_eq deriv_add_const deriv_log
deriv2_negMulLog 📖	mathematical	—	Nat.iterate deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace negMulLog instNeg instInv	—	negMulLog_eq_neg deriv2_mul_log deriv.fun_neg'
deriv_mul_log 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul log instAdd instOne	—	deriv_fun_mul deriv_id'' one_mul deriv_log' mul_inv_cancel₀
deriv_mul_log_zero 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul log instZero	—	deriv_zero_of_not_differentiableAt not_DifferentiableAt_log_mul_zero
deriv_negMulLog 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace negMulLog instSub instNeg log instOne	—	negMulLog_eq_neg deriv.fun_neg deriv_mul_log Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf
differentiableAt_negMulLog 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace negMulLog	—	differentiableAt_negMulLog_iff
differentiableAt_negMulLog_iff 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace negMulLog	—	not_DifferentiableAt_log_mul_zero neg_mul differentiableOn_negMulLog DifferentiableWithinAt.differentiableAt T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal
differentiableOn_mul_log 📖	mathematical	—	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul log Compl.compl Set Set.instCompl Set.instSingletonSet instZero	—	DifferentiableOn.mul Differentiable.differentiableOn differentiable_id differentiableOn_log
differentiableOn_negMulLog 📖	mathematical	—	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace negMulLog Compl.compl Set Set.instCompl Set.instSingletonSet instZero	—	negMulLog_eq_neg DifferentiableOn.neg differentiableOn_mul_log
hasDerivAt_mul_log 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal log instAdd instOne	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal deriv_mul_log IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul hasDerivAt_deriv_iff DifferentiableOn.differentiableAt differentiableOn_mul_log T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal
hasDerivAt_negMulLog 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal negMulLog instSub instNeg log instOne	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal deriv_negMulLog IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul hasDerivAt_deriv_iff DifferentiableOn.differentiableAt differentiableOn_negMulLog T5Space.toT1Space OrderTopology.t5Space instOrderTopologyReal
leftDeriv_mul_log 📖	mathematical	—	derivWithin Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul log Set.Iio instPreorder instAdd instOne	—	HasDerivWithinAt.derivWithin HasDerivAt.hasDerivWithinAt hasDerivAt_mul_log uniqueDiffWithinAt_Iio
mul_log_nonneg 📖	mathematical	Real instLE instOne	Real instLE instZero instMul log	—	mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing LE.le.trans zero_le_one instZeroLEOneClass log_nonneg
mul_log_nonpos 📖	mathematical	Real instLE instZero instOne	Real instLE instMul log instZero	—	mul_nonpos_of_nonneg_of_nonpos IsOrderedRing.toPosMulMono instIsOrderedRing log_nonpos
negMulLog_def 📖	mathematical	—	negMulLog Real instMul instNeg log	—	—
negMulLog_eq_neg 📖	mathematical	—	negMulLog Real instNeg instMul log	—	neg_mul
negMulLog_mul 📖	mathematical	—	negMulLog Real instMul instAdd	—	neg_mul MulZeroClass.zero_mul log_zero MulZeroClass.mul_zero neg_zero mul_neg add_zero log_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero
negMulLog_nonneg 📖	mathematical	Real instLE instZero instOne	Real instLE instZero negMulLog	—	negMulLog_eq_neg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_log_nonpos
negMulLog_one 📖	mathematical	—	negMulLog Real instOne instZero	—	log_one MulZeroClass.mul_zero
negMulLog_zero 📖	mathematical	—	negMulLog Real instZero	—	neg_zero log_zero MulZeroClass.mul_zero
not_DifferentiableAt_log_mul_zero 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul log instZero	—	not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi DifferentiableAt.differentiableWithinAt
not_continuousAt_deriv_mul_log_zero 📖	mathematical	—	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace deriv DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace instMul log instZero	—	not_continuousAt_of_tendsto nhdsGT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing instNoMaxOrderOfNontrivial instIsOrderedRing instNontrivial nhdsWithin_le_nhds instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal instIsOrderedAddMonoid instNoBotOrderOfNoMinOrder instNoMinOrderOfNontrivial
rightDeriv_mul_log 📖	mathematical	—	derivWithin Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul log Set.Ioi instPreorder instAdd instOne	—	HasDerivWithinAt.derivWithin HasDerivAt.hasDerivWithinAt hasDerivAt_mul_log uniqueDiffWithinAt_Ioi
strictConcaveOn_negMulLog 📖	mathematical	—	StrictConcaveOn Real semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici instPreorder instZero negMulLog	—	negMulLog_eq_neg StrictConvexOn.neg instIsOrderedAddMonoid strictConvexOn_mul_log
strictConvexOn_mul_log 📖	mathematical	—	StrictConvexOn Real semiring partialOrder instAddCommMonoid Algebra.toSMul instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici instPreorder instZero instMul log	—	strictConvexOn_of_deriv2_pos convex_Ici instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instIsStrictOrderedRing Continuous.continuousOn continuous_mul_log deriv2_mul_log inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono interior_Ici' instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered instNoMinOrderOfNontrivial instIsOrderedRing instNontrivial
tendsto_deriv_mul_log_atTop 📖	mathematical	—	Filter.Tendsto Real deriv DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul log Filter.atTop instPreorder	—	Filter.tendsto_congr' Filter.EventuallyEq.eq_1 Filter.eventually_atTop instIsDirectedOrder instIsOrderedRing instArchimedean deriv_mul_log LT.lt.ne' LT.lt.trans_le zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.Tendsto.atTop_add instIsOrderedAddMonoid instOrderTopologyReal tendsto_log_atTop tendsto_const_nhds
tendsto_rightDeriv_mul_log_atTop 📖	mathematical	—	Filter.Tendsto Real derivWithin DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instMul log Set.Ioi instPreorder Filter.atTop	—	Filter.tendsto_congr' Filter.EventuallyEq.eq_1 Filter.eventually_atTop instIsDirectedOrder instIsOrderedRing instArchimedean rightDeriv_mul_log LT.lt.ne' LT.lt.trans_le zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.Tendsto.atTop_add instIsOrderedAddMonoid instOrderTopologyReal tendsto_log_atTop tendsto_const_nhds

Real.Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_log 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Real.log	—	Continuous.comp Real.continuous_mul_log

---

← Back to Index