Log

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

Statistics

Metric	Count
Definitions `expOpenPartialHomeomorph`, `expPartialHomeomorph`	2
Theorems `continuousWithinAt_log_of_re_neg_of_im_zero`, `countable_preimage_exp`, `exp_eq_exp_iff_exists_int`, `exp_eq_exp_iff_exp_sub_eq_one`, `exp_eq_one_iff`, `exp_inj_of_neg_pi_lt_of_le_pi`, `exp_log`, `log_I`, `log_conj`, `log_conj_eq_ite`, `log_div_self`, `log_exp`, `log_exp_eq_re_add_toIocMod`, `log_exp_eq_sub_toIocDiv`, `log_exp_exists`, `log_im`, `log_im_le_pi`, `log_inv`, `log_inv_eq_ite`, `log_mul`, `log_mul_eq_add_log_iff`, `log_mul_ofReal`, `log_neg_I`, `log_neg_one`, `log_ofReal_mul`, `log_ofReal_re`, `log_one`, `log_re`, `log_zero`, `map_exp_comap_re_atBot`, `map_exp_comap_re_atTop`, `natCast_log`, `neg_pi_lt_log_im`, `ofNat_log`, `ofReal_log`, `range_exp`, `re_eq_re_of_cexp_eq_cexp`, `tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero`, `tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero`, `two_pi_I_ne_zero`, `clog`, `clog`, `clog`, `clog`, `clog`, `preimage_cexp`, `continuousAt_clog`	47
Total	49

Complex

Definitions

Name	Category	Theorems
`expOpenPartialHomeomorph` 📖	CompOp	—
`expPartialHomeomorph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousWithinAt_log_of_re_neg_of_im_zero` 📖	mathematical	`Real` `Real.instLT` `re` `Real.instZero` `im`	`ContinuousWithinAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `log` `setOf` `Real` `Real.instLE` `Real.instZero` `im`	—	`Filter.Tendsto.add` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousWithinAt.tendsto` `ContinuousAt.comp_continuousWithinAt` `Continuous.continuousAt` `continuous_ofReal` `ContinuousWithinAt.log` `Continuous.continuousWithinAt` `continuous_norm` `CanLift.prf` `canLift` `norm_real` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `LT.lt.ne` `ContinuousWithinAt.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `continuousWithinAt_arg_of_re_neg_of_im_zero` `tendsto_const_nhds`
`countable_preimage_exp` 📖	mathematical	—	`Set.Countable` `Complex` `Set.preimage` `exp`	—	`Set.Countable.mono` `Set.image_preimage_eq_inter_range` `range_exp` `Set.diff_eq` `Set.union_singleton` `Set.diff_union_self` `Set.subset_union_left` `Set.Countable.insert` `Set.Countable.image` `Set.biUnion_preimage_singleton` `Set.Countable.biUnion` `Nat.instAtLeastTwoHAddOfNat` `Set.setOf_exists` `Set.countable_iUnion` `instCountableInt` `Set.countable_singleton`
`exp_eq_exp_iff_exists_int` 📖	mathematical	—	`exp` `Complex` `instAdd` `instMul` `instIntCast` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I`	—	`Nat.instAtLeastTwoHAddOfNat`
`exp_eq_exp_iff_exp_sub_eq_one` 📖	mathematical	—	`exp` `Complex` `instSub` `instOne`	—	`exp_sub` `div_eq_one_iff_eq` `exp_ne_zero`
`exp_eq_one_iff` 📖	mathematical	—	`exp` `Complex` `instOne` `instMul` `instIntCast` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I`	—	`Nat.instAtLeastTwoHAddOfNat` `existsUnique_add_zsmul_mem_Ioc` `Real.instIsOrderedAddMonoid` `Real.instArchimedean` `Real.two_pi_pos` `Int.cast_neg` `neg_mul` `eq_neg_iff_add_eq_zero` `two_mul` `mul_one` `add_zero` `MulZeroClass.mul_zero` `mul_add` `Distrib.leftDistribClass` `sub_self` `neg_add_cancel_left` `smul_add` `zsmul_eq_mul` `log_exp` `Function.Periodic.int_mul` `exp_periodic` `log_one` `Function.Periodic.eq` `exp_zero`
`exp_inj_of_neg_pi_lt_of_le_pi` 📖	—	`Real` `Real.instLT` `Real.instNeg` `Real.pi` `im` `Real.instLE` `exp`	—	—	`log_exp`
`exp_log` 📖	mathematical	—	`exp` `log`	—	`log.eq_1` `exp_add_mul_I` `ofReal_sin` `sin_arg` `ofReal_cos` `cos_arg` `ofReal_exp` `Real.exp_log` `norm_pos_iff` `mul_add` `Distrib.leftDistribClass` `ofReal_div` `mul_div_cancel₀` `ofReal_ne_zero` `norm_ne_zero_iff` `mul_assoc` `re_add_im`
`log_I` 📖	mathematical	—	`log` `I` `Complex` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid` `ofReal` `Real.pi` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `norm_I` `Real.log_one` `arg_I` `ofReal_div` `zero_add`
`log_conj` 📖	mathematical	—	`log` `DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `starRingEnd` `instStarRing`	—	`log_conj_eq_ite`
`log_conj_eq_ite` 📖	mathematical	—	`log` `DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `starRingEnd` `instStarRing` `Real` `arg` `Real.pi` `Real.decidableEq`	—	`norm_conj` `arg_conj` `map_add` `SemilinearMapClass.toAddHomClass` `instCharZero` `RingHomClass.toLinearMapClassNNRat` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `conj_ofReal` `ofReal_neg` `conj_I` `mul_neg` `neg_mul`
`log_div_self` 📖	mathematical	—	`log` `Complex` `DivInvMonoid.toDiv` `instDivInvMonoid` `instZero`	—	`norm_div` `Real.log_div_self` `arg_div_self` `MulZeroClass.zero_mul` `add_zero`
`log_exp` 📖	mathematical	`Real` `Real.instLT` `Real.instNeg` `Real.pi` `im` `Real.instLE`	`log` `exp`	—	`log.eq_1` `norm_exp` `Real.log_exp` `exp_eq_exp_re_mul_sin_add_cos` `ofReal_exp` `arg_mul_cos_add_sin_mul_I` `Real.exp_pos` `re_add_im`
`log_exp_eq_re_add_toIocMod` 📖	mathematical	—	`log` `exp` `Complex` `instAdd` `ofReal` `re` `instMul` `toIocMod` `Real` `Real.instAddCommGroup` `Real.linearOrder` `Real.instIsOrderedAddMonoid` `Real.instArchimedean` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Real.two_pi_pos` `Real.instNeg` `im` `I`	—	`Real.instIsOrderedAddMonoid` `Real.instArchimedean` `Nat.instAtLeastTwoHAddOfNat` `Real.two_pi_pos` `log.eq_1` `norm_exp` `Real.log_exp` `arg_exp`
`log_exp_eq_sub_toIocDiv` 📖	mathematical	—	`log` `exp` `Complex` `instSub` `instMul` `instIntCast` `toIocDiv` `Real` `Real.instAddCommGroup` `Real.linearOrder` `Real.instIsOrderedAddMonoid` `Real.instArchimedean` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.pi` `Real.two_pi_pos` `Real.instNeg` `im` `instNatCast` `ofReal` `I`	—	`Real.instIsOrderedAddMonoid` `Real.instArchimedean` `Nat.instAtLeastTwoHAddOfNat` `Real.two_pi_pos` `log_exp_eq_re_add_toIocMod` `toIocMod.eq_1` `ofReal_sub` `sub_mul` `add_sub_assoc` `re_add_im` `zsmul_eq_mul` `ofReal_mul` `mul_assoc`
`log_exp_exists` 📖	mathematical	—	`log` `exp` `Complex` `instAdd` `instMul` `instIntCast` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I`	—	`Nat.instAtLeastTwoHAddOfNat` `exp_eq_exp_iff_exists_int` `exp_log` `exp_ne_zero`
`log_im` 📖	mathematical	—	`im` `log` `arg`	—	`mul_one` `MulZeroClass.mul_zero` `add_zero` `zero_add`
`log_im_le_pi` 📖	mathematical	—	`Real` `Real.instLE` `im` `log` `Real.pi`	—	`log_im`
`log_inv` 📖	mathematical	—	`log` `Complex` `instInv` `instNeg`	—	`log_inv_eq_ite`
`log_inv_eq_ite` 📖	mathematical	—	`log` `Complex` `instInv` `Real` `arg` `Real.pi` `Real.decidableEq` `instNeg` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring` `RingHom.instFunLike` `starRingEnd` `instStarRing`	—	`inv_zero` `log_zero` `arg_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `neg_zero` `inv_def` `log_mul_ofReal` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `normSq_pos` `map_ne_zero` `instNontrivial` `Real.log_inv` `ofReal_neg` `sub_eq_neg_add` `log_conj_eq_ite` `map_add` `SemilinearMapClass.toAddHomClass` `instCharZero` `RingHomClass.toLinearMapClassNNRat` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `conj_ofReal` `conj_I` `normSq_eq_norm_sq` `Real.log_pow` `Nat.instAtLeastTwoHAddOfNat` `ofReal_mul` `neg_add` `mul_neg` `neg_neg`
`log_mul` 📖	mathematical	`Real` `Set` `Set.instMembership` `Set.Ioc` `Real.instPreorder` `Real.instNeg` `Real.pi` `Real.instAdd` `arg`	`log` `Complex` `instMul` `instAdd`	—	`log_mul_eq_add_log_iff`
`log_mul_eq_add_log_iff` 📖	mathematical	—	`log` `Complex` `instMul` `instAdd` `Real` `Set` `Set.instMembership` `Set.Ioc` `Real.instPreorder` `Real.instNeg` `Real.pi` `Real.instAdd` `arg`	—	`ext_iff` `log_re` `log_im` `norm_mul` `NormedDivisionRing.toNormMulClass` `Real.log_mul` `norm_ne_zero_iff` `arg_mul_eq_add_arg_iff`
`log_mul_ofReal` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`log` `Complex` `instMul` `ofReal` `instAdd` `Real.log`	—	`mul_comm` `log_ofReal_mul`
`log_neg_I` 📖	mathematical	—	`log` `Complex` `instNeg` `I` `instMul` `DivInvMonoid.toDiv` `instDivInvMonoid` `ofReal` `Real.pi` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `norm_neg` `norm_I` `Real.log_one` `arg_neg_I` `ofReal_neg` `ofReal_div` `neg_mul` `zero_add`
`log_neg_one` 📖	mathematical	—	`log` `Complex` `instNeg` `instOne` `instMul` `ofReal` `Real.pi` `I`	—	`norm_neg` `CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `Real.log_one` `arg_neg_one` `zero_add`
`log_ofReal_mul` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`log` `Complex` `instMul` `ofReal` `instAdd` `Real.log`	—	`norm_ne_zero_iff` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_real` `arg_real_mul` `Real.norm_of_nonneg` `LT.lt.le` `Real.log_mul` `LT.lt.ne'` `ofReal_add` `add_assoc`
`log_ofReal_re` 📖	mathematical	—	`re` `log` `ofReal` `Real.log`	—	`log_re` `norm_real` `Real.log_abs`
`log_one` 📖	mathematical	—	`log` `Complex` `instOne` `instZero`	—	`CStarRing.norm_of_mem_unitary` `RCLike.instCStarRing` `instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `Real.log_one` `arg_one` `MulZeroClass.zero_mul` `add_zero`
`log_re` 📖	mathematical	—	`re` `log` `Real.log` `Norm.norm` `Complex` `instNorm`	—	`MulZeroClass.mul_zero` `mul_one` `sub_self` `add_zero`
`log_zero` 📖	mathematical	—	`log` `Complex` `instZero`	—	`norm_zero` `Real.log_zero` `arg_zero` `MulZeroClass.zero_mul` `add_zero`
`map_exp_comap_re_atBot` 📖	mathematical	—	`Filter.map` `Complex` `exp` `Filter.comap` `Real` `re` `Filter.atBot` `Real.instPreorder` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instZero` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`comap_exp_nhds_zero` `Filter.map_comap` `range_exp` `nhdsWithin.eq_1`
`map_exp_comap_re_atTop` 📖	mathematical	—	`Filter.map` `Complex` `exp` `Filter.comap` `Real` `re` `Filter.atTop` `Real.instPreorder` `Bornology.cobounded` `PseudoMetricSpace.toBornology` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField`	—	`comap_exp_cobounded` `Filter.map_comap` `range_exp` `inf_eq_left` `Filter.le_principal_iff` `Bornology.eventually_ne_cobounded`
`natCast_log` 📖	mathematical	—	`ofReal` `Real.log` `Real` `Real.instNatCast` `log` `Complex` `instNatCast`	—	`ofReal_log` `Nat.cast_nonneg` `Real.instIsOrderedRing` `ofReal_natCast`
`neg_pi_lt_log_im` 📖	mathematical	—	`Real` `Real.instLT` `Real.instNeg` `Real.pi` `im` `log`	—	`log_im`
`ofNat_log` 📖	mathematical	—	`ofReal` `Real.log` `log` `Complex` `instOfNatAtLeastTwo` `instNatCast`	—	`natCast_log`
`ofReal_log` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`ofReal` `Real.log` `log`	—	`ext` `log_re` `ofReal_re` `norm_of_nonneg` `ofReal_im` `log_im` `arg_ofReal_of_nonneg`
`range_exp` 📖	mathematical	—	`Set.range` `Complex` `exp` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `instZero`	—	`Set.ext` `exp_ne_zero` `exp_log`
`re_eq_re_of_cexp_eq_cexp` 📖	mathematical	`exp`	`re`	—	`Nat.instAtLeastTwoHAddOfNat` `exp_eq_exp_iff_exists_int` `MulZeroClass.mul_zero` `sub_zero` `MulZeroClass.zero_mul` `add_zero` `mul_one` `sub_self`
`tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero` 📖	mathematical	`Real` `Real.instLT` `re` `Real.instZero` `im`	`Filter.Tendsto` `Complex` `log` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `setOf` `Real` `Real.instLT` `im` `Real.instZero` `nhds` `instSub` `ofReal` `Real.log` `Norm.norm` `instNorm` `instMul` `Real.pi` `I`	—	`sub_eq_add_neg` `ofReal_neg` `neg_mul` `Filter.Tendsto.add` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousWithinAt.tendsto` `ContinuousAt.comp_continuousWithinAt` `Continuous.continuousAt` `continuous_ofReal` `ContinuousWithinAt.log` `Continuous.continuousWithinAt` `continuous_norm` `CanLift.prf` `canLift` `norm_real` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `LT.lt.ne` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `Filter.Tendsto.comp` `Continuous.tendsto` `tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero` `tendsto_const_nhds`
`tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero` 📖	mathematical	`Real` `Real.instLT` `re` `Real.instZero` `im`	`Filter.Tendsto` `Complex` `log` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `setOf` `Real` `Real.instLE` `Real.instZero` `im` `nhds` `instAdd` `ofReal` `Real.log` `Norm.norm` `instNorm` `instMul` `Real.pi` `I`	—	`arg_eq_pi_iff` `ContinuousWithinAt.tendsto` `continuousWithinAt_log_of_re_neg_of_im_zero`
`two_pi_I_ne_zero` 📖	—	—	—	—	`Nat.instAtLeastTwoHAddOfNat` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `instCharZero`

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clog` 📖	mathematical	`Continuous` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership` `Complex.slitPlane`	`Continuous` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.log`	—	`continuous_iff_continuousAt` `ContinuousAt.clog` `continuousAt`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clog` 📖	mathematical	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership` `Complex.slitPlane`	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.log`	—	`Filter.Tendsto.clog`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clog` 📖	mathematical	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership` `Complex.slitPlane`	`ContinuousOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.log`	—	`ContinuousWithinAt.clog`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clog` 📖	mathematical	`ContinuousWithinAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership` `Complex.slitPlane`	`ContinuousWithinAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.log`	—	`Filter.Tendsto.clog`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clog` 📖	mathematical	`Filter.Tendsto` `Complex` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Set` `Set.instMembership` `Complex.slitPlane`	`Filter.Tendsto` `Complex` `Complex.log` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	—	`comp` `ContinuousAt.tendsto` `continuousAt_clog`

Set.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_cexp` 📖	mathematical	—	`Set.Countable` `Complex` `Set.preimage` `Complex.exp`	—	`Complex.countable_preimage_exp`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_clog` 📖	mathematical	`Complex` `Set` `Set.instMembership` `Complex.slitPlane`	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `Complex.log`	—	`ContinuousAt.add` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousAt.comp` `Continuous.continuousAt` `Complex.continuous_ofReal` `Real.continuousAt_log` `norm_ne_zero_iff` `Complex.slitPlane_ne_zero` `continuous_norm` `continuous_mul_const` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Complex.continuousAt_arg`

---

← Back to Index