Auxiliary

📁 Source: PrimeNumberTheoremAnd/Auxiliary.lean

Statistics

Metric	Count
Definitions	0
Theorems deriv_ofReal, differentiableAt_ofReal, differentiable_ofReal, hasDerivAt_ofReal, comp_ofReal, ofReal_comp, ofReal_comp_iff, comp_ofReal, ofReal_comp, ofReal_comp_iff, of_hasDerivAt_ofReal_comp, comp_ofReal, ofReal_comp	13
Total	13

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv_ofReal 📖	—	—	—	—	hasDerivAt_ofReal
differentiableAt_ofReal 📖	—	—	—	—	hasDerivAt_ofReal
differentiable_ofReal 📖	—	—	—	—	—
hasDerivAt_ofReal 📖	—	—	—	—	—

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_ofReal 📖	—	—	—	—	DifferentiableAt.comp_ofReal
ofReal_comp 📖	—	—	—	—	DifferentiableAt.ofReal_comp
ofReal_comp_iff 📖	—	—	—	—	DifferentiableAt.ofReal_comp_iff

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_ofReal 📖	—	—	—	—	—
ofReal_comp 📖	—	—	—	—	—
ofReal_comp_iff 📖	—	—	—	—	HasDerivAt.of_hasDerivAt_ofReal_comp ofReal_comp

HasDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_hasDerivAt_ofReal_comp 📖	—	—	—	—	—

deriv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_ofReal 📖	—	—	—	—	—
ofReal_comp 📖	—	—	—	—	DifferentiableAt.ofReal_comp_iff

---

← Back to Index