InvLog

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

Statistics

Metric	Count
Definitions	0
Theorems deriv_inv_log, not_continuousAt_inv_log_neg_one, not_continuousAt_inv_log_one, not_differentiableAt_inv_log_zero	4
Total	4

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_inv_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 instInv log DivInvMonoid.toDiv instDivInvMonoid instNeg Monoid.toNatPow instMonoid	—	eq_or_ne inv_zero neg_zero log_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat div_zero deriv_zero_of_not_differentiableAt not_differentiableAt_inv_log_zero inv_one log_one DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul not_continuousAt_inv_log_one inv_neg neg_neg log_neg_eq_log not_continuousAt_inv_log_neg_one deriv_fun_inv'' deriv_log'
not_continuousAt_inv_log_neg_one 📖	mathematical	—	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instInv log instNeg instOne	—	not_continuousAt_inv_log_one log_neg_eq_log ContinuousAt.comp' continuousAt_neg IsTopologicalRing.toContinuousNeg instIsTopologicalRingReal
not_continuousAt_inv_log_one 📖	mathematical	—	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instInv log instOne	—	HasDerivAt.tendsto_nhdsNE ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasDerivAt.congr_simp inv_one hasDerivAt_log one_ne_zero NeZero.charZero_one RCLike.charZero_rclike Filter.Tendsto.comp Filter.tendsto_inv₀_nhdsNE_zero log_one not_continuousAt_of_tendsto PerfectSpace.not_isolated instPerfectSpace nhdsWithin_le_nhds Metric.disjoint_nhds_cobounded
not_differentiableAt_inv_log_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 instInv log instZero	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul zero_add log_zero inv_zero sub_zero mul_comm tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within tendsto_log_mul_self_nhdsLT_zero nhdsWithin_Ioo_eq_nhdsLT neg_one_lt_zero instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal instIsOrderedAddMonoid instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono eventually_nhdsWithin_of_forall mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le log_neg log_neg_eq_log Filter.Tendsto.not_tendsto tendsto_nhdsWithin_mono_left nhdsLT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial instIsOrderedRing instNontrivial instClosedIciTopology instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Filter.Tendsto.comp tendsto_inv_nhdsGT_zero

---

← Back to Index