RemovableSingularity

📁 Source: Mathlib/Analysis/Complex/RemovableSingularity.lean

Statistics

Metric	Count
Definitions	0
Theorems analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt, differentiableOn_compl_singleton_and_continuousAt_iff, differentiableOn_dslope, differentiableOn_update_limUnder_insert_of_isLittleO, differentiableOn_update_limUnder_of_bddAbove, differentiableOn_update_limUnder_of_isLittleO, tendsto_limUnder_of_differentiable_on_punctured_nhds_of_bounded_under, tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO, two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable	9
Total	9

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt 📖	mathematical	Filter.Eventually Complex DifferentiableAt DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet ContinuousAt	AnalyticAt instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike RCLike.innerProductSpace	—	Filter.HasBasis.mem_iff nhdsWithin_hasBasis Metric.nhds_basis_closedBall CanLift.prf NNReal.canLift LT.lt.le ContinuousAt.continuousWithinAt eq_or_ne DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasFPowerSeriesOnBall.analyticAt hasFPowerSeriesOnBall_of_differentiable_off_countable Set.countable_singleton Set.diff_subset_diff_left Metric.ball_subset_closedBall
differentiableOn_compl_singleton_and_continuousAt_iff 📖	mathematical	Set Complex Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField	DifferentiableOn DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.instSDiff Set.instSingletonSet ContinuousAt	—	eq_or_ne DifferentiableAt.differentiableWithinAt AnalyticAt.differentiableAt analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt eventually_nhdsWithin_iff Filter.Eventually.mono eventually_mem_nhds_iff DifferentiableOn.differentiableAt Filter.inter_mem IsOpen.mem_nhds isOpen_ne T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Ne.nhdsWithin_diff_singleton DifferentiableOn.mono Set.diff_subset DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
differentiableOn_dslope 📖	mathematical	Set Complex Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField	DifferentiableOn DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace dslope	—	DifferentiableOn.of_dslope differentiableOn_compl_singleton_and_continuousAt_iff differentiableOn_dslope_of_notMem DifferentiableOn.mono Set.diff_subset continuousAt_dslope_same DifferentiableOn.differentiableAt
differentiableOn_update_limUnder_insert_of_isLittleO 📖	mathematical	Set Complex Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Compl.compl Set.instCompl Set.instSingletonSet DifferentiableOn DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Asymptotics.IsLittleO NormedAddCommGroup.toNorm instNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup instInv instSub	Function.update instDecidableEq limUnder AddTorsor.nonempty SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor Set.instInsert	—	differentiableOn_update_limUnder_of_isLittleO insert_mem_nhds_iff DifferentiableOn.mono
differentiableOn_update_limUnder_of_bddAbove 📖	mathematical	Set Complex Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DifferentiableOn DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.instSDiff Set.instSingletonSet BddAbove Real Real.instLE Set.image Norm.norm NormedAddCommGroup.toNorm	Function.update instDecidableEq limUnder AddTorsor.nonempty SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor nhdsWithin Compl.compl Set.instCompl	—	differentiableOn_update_limUnder_of_isLittleO Filter.IsBoundedUnder.isLittleO_sub_self_inv Filter.eventually_map mem_nhdsWithin_iff_exists_mem_nhds_inter norm_sub_le_of_le Set.mem_image_of_mem le_rfl
differentiableOn_update_limUnder_of_isLittleO 📖	mathematical	Set Complex Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DifferentiableOn DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.instSDiff Set.instSingletonSet Asymptotics.IsLittleO NormedAddCommGroup.toNorm instNorm nhdsWithin Compl.compl Set.instCompl SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup instInv instSub	Function.update instDecidableEq limUnder AddTorsor.nonempty SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor	—	DifferentiableOn.smul NormedSpace.toIsBoundedSMul IsScalarTower.left DifferentiableOn.sub_const differentiableOn_id continuousWithinAt_compl_self Asymptotics.IsLittleO.tendsto_inv_smul_nhds_zero NormedSpace.toNormSMulClass Filter.Tendsto.smul IsBoundedSMul.continuousSMul Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousWithinAt.tendsto continuousWithinAt_id tendsto_const_nhds inv_inv sub_add_cancel zero_add Filter.Tendsto.add IsTopologicalAddGroup.toContinuousAdd continuousAt_update_same ContinuousOn.continuousAt DifferentiableOn.continuousOn IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology dslope_sub_smul differentiableOn_dslope differentiableOn_compl_singleton_and_continuousAt_iff AddTorsor.nonempty Filter.Tendsto.limUnder_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace PerfectSpace.not_isolated instPerfectSpace
tendsto_limUnder_of_differentiable_on_punctured_nhds_of_bounded_under 📖	mathematical	Filter.Eventually Complex DifferentiableAt DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet Filter.IsBoundedUnder Real Real.instLE Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	Filter.Tendsto nhds limUnder AddTorsor.nonempty SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor	—	tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO Filter.IsBoundedUnder.isLittleO_sub_self_inv
tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO 📖	mathematical	Filter.Eventually Complex DifferentiableAt DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet Asymptotics.IsLittleO NormedAddCommGroup.toNorm instNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup instInv instSub	Filter.Tendsto nhds limUnder AddTorsor.nonempty SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor	—	DifferentiableAt.differentiableWithinAt AddTorsor.nonempty differentiableOn_update_limUnder_of_isLittleO eventually_nhdsWithin_iff continuousAt_update_same DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul DifferentiableOn.differentiableAt
two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable 📖	mathematical	IsOpen Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Set Set.instHasSubset Metric.closedBall DifferentiableOn DenselyNormedField.toNontriviallyNormedField instDenselyNormedField addCommGroup instModuleSelf NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.instMembership Metric.ball	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid instInv instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat ofReal Real.pi I circleIntegral Monoid.toNatPow instSub deriv	—	differentiableOn_dslope IsOpen.mem_nhds HasSubset.Subset.trans Set.instIsTransSubset Metric.ball_subset_closedBall Nat.instAtLeastTwoHAddOfNat DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul DifferentiableOn.diffContOnCl_ball dslope_same ContinuousOn.inv₀ IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing Continuous.continuousOn Continuous.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing Continuous.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_id' continuous_const Disjoint.ne_of_mem Metric.sphere_disjoint_ball sub_eq_zero sq_eq_zero_iff isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass ContinuousOn.circleIntegrable LT.lt.le Metric.pos_of_mem_ball ContinuousOn.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousOn.mono DifferentiableOn.continuousOn IsTopologicalSemiring.toContinuousAdd IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalAddGroup.toContinuousAdd Metric.sphere_subset_closedBall continuousOn_const zpow_neg circleIntegral.integral_sub_zpow_of_ne smul_sub circleIntegral.integral_sub circleIntegral.integral_smul_const zero_smul sub_zero circleIntegral.integral_congr sq mul_inv dslope_of_ne IsScalarTower.left

---

← Back to Index