Arsinh

📁 Source: Mathlib/Analysis/SpecialFunctions/Arsinh.lean

Statistics

Metric	Count
Definitions arsinh, sinhEquiv, sinhHomeomorph, sinhOrderIso	4
Theorems arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, arsinh, analyticAt_arsinh, analyticOnNhd_arsinh, analyticOn_arsinh, analyticWithinAt_arsinh, arsinh_bijective, arsinh_eq_zero_iff, arsinh_inj, arsinh_injective, arsinh_le_arsinh, arsinh_lt_arsinh, arsinh_neg, arsinh_neg_iff, arsinh_nonneg_iff, arsinh_nonpos_iff, arsinh_pos_iff, arsinh_sinh, arsinh_strictMono, arsinh_surjective, arsinh_zero, contDiff_arsinh, continuous_arsinh, cosh_arsinh, differentiable_arsinh, exp_arsinh, hasDerivAt_arsinh, hasStrictDerivAt_arsinh, sinhEquiv_apply, sinhEquiv_symm_apply, sinhHomeomorph_apply, sinhHomeomorph_symm_apply, sinhOrderIso_apply, sinhOrderIso_symm_apply, sinh_arsinh, sinh_bijective, sinh_surjective, tanh_arsinh	55
Total	59

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField WithTop.some ENat	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField WithTop.some ENat Real.arsinh	—	comp Real.contDiff_arsinh

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField WithTop.some ENat	ContDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField WithTop.some ENat Real.arsinh	—	comp ContDiff.contDiffAt Real.contDiff_arsinh

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField WithTop.some ENat	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField WithTop.some ENat Real.arsinh	—	ContDiffWithinAt.arsinh

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	ContDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField WithTop.some ENat	ContDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField WithTop.some ENat Real.arsinh	—	ContDiffAt.comp_contDiffWithinAt ContDiff.contDiffAt Real.contDiff_arsinh

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.arsinh	—	comp Real.continuous_arsinh

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.arsinh	—	Filter.Tendsto.arsinh

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.arsinh	—	ContinuousWithinAt.arsinh

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	ContinuousWithinAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	ContinuousWithinAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.arsinh	—	Filter.Tendsto.arsinh

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.pseudoMetricSpace	Differentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.pseudoMetricSpace Real.arsinh	—	comp Real.differentiable_arsinh

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.pseudoMetricSpace	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.pseudoMetricSpace Real.arsinh	—	comp Real.differentiable_arsinh

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.pseudoMetricSpace	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.pseudoMetricSpace Real.arsinh	—	DifferentiableWithinAt.arsinh

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	DifferentiableWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.pseudoMetricSpace	DifferentiableWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Real.pseudoMetricSpace Real.arsinh	—	DifferentiableAt.comp_differentiableWithinAt Real.differentiable_arsinh

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	Filter.Tendsto Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Filter.Tendsto Real Real.arsinh nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	comp Continuous.tendsto Real.continuous_arsinh

HasDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.arsinh Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instInv Real.sqrt Real.instAdd Real.instOne Monoid.toPow Real.instMonoid	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal comp Real.hasDerivAt_arsinh

HasDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	HasDerivWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal	HasDerivWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.arsinh Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instInv Real.sqrt Real.instAdd Real.instOne Monoid.toPow Real.instMonoid	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasDerivAt.comp_hasDerivWithinAt Real.hasDerivAt_arsinh

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace	HasFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace Real.arsinh StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.instSMul RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Real.instInv Real.sqrt Real.instAdd Real.instOne Monoid.toPow Real.instMonoid	—	HasDerivAt.comp_hasFDerivAt Real.hasDerivAt_arsinh

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	HasFDerivWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace	HasFDerivWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace Real.arsinh StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.instSMul RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Real.instInv Real.sqrt Real.instAdd Real.instOne Monoid.toPow Real.instMonoid	—	HasDerivAt.comp_hasFDerivWithinAt Real.hasDerivAt_arsinh

HasStrictDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	HasStrictDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal	HasStrictDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instMul IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.arsinh Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Real.instInv Real.sqrt Real.instAdd Real.instOne Monoid.toPow Real.instMonoid	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal comp Real.hasStrictDerivAt_arsinh

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arsinh 📖	mathematical	HasStrictFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace	HasStrictFDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace Real.arsinh StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.instSMul RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Real.instInv Real.sqrt Real.instAdd Real.instOne Monoid.toPow Real.instMonoid	—	HasStrictDerivAt.comp_hasStrictFDerivAt Real.hasStrictDerivAt_arsinh

Real

Definitions

Name	Category	Theorems
arsinh 📖	CompOp	50 math math: Differentiable.arsinh, arsinh_surjective, ContDiffAt.arsinh, arsinh_zero, arsinh_neg, arsinh_injective, HasStrictFDerivAt.arsinh, hasDerivAt_arsinh, arsinh_nonpos_iff, arsinh_nonneg_iff, sinh_arsinh, HasDerivWithinAt.arsinh, sinhEquiv_symm_apply, arsinh_pos_iff, exp_arsinh, contDiff_arsinh, arsinh_lt_arsinh, UpperHalfPlane.dist_eq, analyticOnNhd_arsinh, hasStrictDerivAt_arsinh, ContinuousWithinAt.arsinh, HasDerivAt.arsinh, arsinh_neg_iff, arsinh_eq_zero_iff, DifferentiableAt.arsinh, HasFDerivWithinAt.arsinh, HasStrictDerivAt.arsinh, arsinh_strictMono, ContinuousOn.arsinh, arsinh_bijective, cosh_arsinh, DifferentiableWithinAt.arsinh, analyticAt_arsinh, HasFDerivAt.arsinh, arsinh_inj, analyticOn_arsinh, ContDiffWithinAt.arsinh, arsinh_sinh, analyticWithinAt_arsinh, differentiable_arsinh, tanh_arsinh, Continuous.arsinh, DifferentiableOn.arsinh, continuous_arsinh, ContinuousAt.arsinh, sinhOrderIso_symm_apply, Filter.Tendsto.arsinh, ContDiff.arsinh, arsinh_le_arsinh, ContDiffOn.arsinh
sinhEquiv 📖	CompOp	2 math math: sinhEquiv_symm_apply, sinhEquiv_apply
sinhHomeomorph 📖	CompOp	2 math math: sinhHomeomorph_symm_apply, sinhHomeomorph_apply
sinhOrderIso 📖	CompOp	3 math math: sinhHomeomorph_symm_apply, sinhOrderIso_apply, sinhOrderIso_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticAt_arsinh 📖	mathematical	—	AnalyticAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField arsinh	—	ContDiffAt.analyticAt ContDiff.contDiffAt contDiff_arsinh
analyticOnNhd_arsinh 📖	mathematical	—	AnalyticOnNhd Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField arsinh	—	analyticAt_arsinh
analyticOn_arsinh 📖	mathematical	—	AnalyticOn Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField arsinh	—	ContDiffOn.analyticOn ContDiff.contDiffOn contDiff_arsinh
analyticWithinAt_arsinh 📖	mathematical	—	AnalyticWithinAt Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField arsinh	—	ContDiffWithinAt.analyticWithinAt ContDiff.contDiffWithinAt contDiff_arsinh
arsinh_bijective 📖	mathematical	—	Function.Bijective Real arsinh	—	Equiv.bijective
arsinh_eq_zero_iff 📖	mathematical	—	arsinh Real instZero	—	arsinh_injective arsinh_zero
arsinh_inj 📖	mathematical	—	arsinh	—	arsinh_injective
arsinh_injective 📖	mathematical	—	Real arsinh	—	Equiv.injective
arsinh_le_arsinh 📖	mathematical	—	Real instLE arsinh	—	OrderIso.le_iff_le
arsinh_lt_arsinh 📖	mathematical	—	Real instLT arsinh	—	OrderIso.lt_iff_lt
arsinh_neg 📖	mathematical	—	arsinh Real instNeg	—	exp_eq_exp exp_arsinh exp_neg eq_inv_of_mul_eq_one_left neg_sq neg_add_eq_sub add_comm mul_comm sq_sub_sq sq_sqrt add_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid zero_le_one instZeroLEOneClass sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono instIsOrderedRing add_sub_cancel_right
arsinh_neg_iff 📖	mathematical	—	Real instLT arsinh instZero	—	lt_iff_lt_of_le_iff_le arsinh_nonneg_iff
arsinh_nonneg_iff 📖	mathematical	—	Real instLE instZero arsinh	—	sinh_le_sinh sinh_zero sinh_arsinh
arsinh_nonpos_iff 📖	mathematical	—	Real instLE arsinh instZero	—	sinh_le_sinh sinh_zero sinh_arsinh
arsinh_pos_iff 📖	mathematical	—	Real instLT instZero arsinh	—	lt_iff_lt_of_le_iff_le arsinh_nonpos_iff
arsinh_sinh 📖	mathematical	—	arsinh sinh	—	sinh_injective sinh_arsinh
arsinh_strictMono 📖	mathematical	—	StrictMono Real instPreorder arsinh	—	OrderIso.strictMono
arsinh_surjective 📖	mathematical	—	Real arsinh	—	Equiv.surjective
arsinh_zero 📖	mathematical	—	arsinh Real instZero	—	zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat add_zero sqrt_one zero_add log_one
contDiff_arsinh 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField arsinh	—	Homeomorph.contDiff_symm_deriv instCompleteSpace LT.lt.ne' cosh_pos hasDerivAt_sinh contDiff_sinh
continuous_arsinh 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace arsinh	—	Homeomorph.continuous
cosh_arsinh 📖	mathematical	—	cosh arsinh sqrt Real instAdd instOne Monoid.toPow instMonoid	—	sqrt_sq LT.lt.le cosh_pos cosh_sq' sinh_arsinh
differentiable_arsinh 📖	mathematical	—	Differentiable Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace arsinh	—	HasDerivAt.differentiableAt hasDerivAt_arsinh
exp_arsinh 📖	mathematical	—	exp arsinh Real instAdd sqrt instOne Monoid.toPow instMonoid	—	exp_log neg_lt_iff_pos_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid lt_sqrt_of_sq_lt Even.neg_pow Nat.instAtLeastTwoHAddOfNat IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
hasDerivAt_arsinh 📖	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 arsinh instInv sqrt instAdd instOne Monoid.toPow instMonoid	—	HasStrictDerivAt.hasDerivAt hasStrictDerivAt_arsinh
hasStrictDerivAt_arsinh 📖	mathematical	—	HasStrictDerivAt 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 arsinh instInv sqrt instAdd instOne Monoid.toPow instMonoid	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing cosh_arsinh OpenPartialHomeomorph.hasStrictDerivAt_symm Set.mem_univ LT.lt.ne' cosh_pos hasStrictDerivAt_sinh
sinhEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Real EquivLike.toFunLike Equiv.instEquivLike sinhEquiv sinh	—	—
sinhEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Real EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sinhEquiv arsinh	—	—
sinhHomeomorph_apply 📖	mathematical	—	DFunLike.coe Homeomorph Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike sinhHomeomorph sinh	—	—
sinhHomeomorph_symm_apply 📖	mathematical	—	DFunLike.coe Homeomorph Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm sinhHomeomorph EquivLike.inv OrderIso Preorder.toLE instPreorder OrderIso.instEquivLike sinhOrderIso	—	—
sinhOrderIso_apply 📖	mathematical	—	DFunLike.coe RelIso Real instLE RelIso.instFunLike sinhOrderIso sinh	—	—
sinhOrderIso_symm_apply 📖	mathematical	—	DFunLike.coe RelIso Real instLE RelIso.instFunLike RelIso.symm sinhOrderIso arsinh	—	—
sinh_arsinh 📖	mathematical	—	sinh arsinh	—	Nat.instAtLeastTwoHAddOfNat sinh_eq arsinh_neg exp_arsinh neg_sq add_sub_add_right_eq_sub sub_neg_eq_add add_self_div_two CharZero.NeZero.two RCLike.charZero_rclike
sinh_bijective 📖	mathematical	—	Function.Bijective Real sinh	—	sinh_injective sinh_surjective
sinh_surjective 📖	mathematical	—	Real sinh	—	Function.LeftInverse.surjective sinh_arsinh
tanh_arsinh 📖	mathematical	—	tanh arsinh Real DivInvMonoid.toDiv instDivInvMonoid sqrt instAdd instOne Monoid.toPow instMonoid	—	tanh_eq_sinh_div_cosh sinh_arsinh cosh_arsinh

---

← Back to Index