Arcosh

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

Statistics

Metric	Count
Definitions arcosh, coshOpenPartialHomeomorph, coshPartialEquiv	3
Theorems add_sqrt_self_sq_sub_one_inv, analyticAt_arcosh, analyticOnNhd_arcosh, analyticOn_arcosh, analyticWithinAt_arcosh, arcosh_bijOn, arcosh_cosh, arcosh_eq_zero_iff, arcosh_injOn, arcosh_le_arcosh, arcosh_lt_arcosh, arcosh_nonneg, arcosh_pos, arcosh_surjOn, arcosh_zero, contDiffAt_arcosh, contDiffOn_arcosh, continuousOn_arcosh, cosh_arcosh, cosh_bijOn, cosh_injOn, cosh_surjOn, differentiableAt_arcosh, differentiableOn_arcosh, exp_arcosh, hasDerivAt_arcosh, hasStrictDerivAt_arcosh, sinh_arcosh, strictMonoOn_arcosh, tanh_arcosh	30
Total	33

Real

Definitions

Name	Category	Theorems
arcosh 📖	CompOp	26 math math: differentiableOn_arcosh, arcosh_bijOn, contDiffAt_arcosh, arcosh_nonneg, arcosh_zero, hasDerivAt_arcosh, sinh_arcosh, tanh_arcosh, exp_arcosh, arcosh_injOn, cosh_arcosh, hasStrictDerivAt_arcosh, analyticOn_arcosh, analyticAt_arcosh, arcosh_pos, strictMonoOn_arcosh, arcosh_cosh, contDiffOn_arcosh, arcosh_le_arcosh, differentiableAt_arcosh, analyticWithinAt_arcosh, arcosh_eq_zero_iff, continuousOn_arcosh, arcosh_surjOn, arcosh_lt_arcosh, analyticOnNhd_arcosh
coshOpenPartialHomeomorph 📖	CompOp	—
coshPartialEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_sqrt_self_sq_sub_one_inv 📖	mathematical	Real instLE instOne	instInv instAdd sqrt instSub Monoid.toNatPow instMonoid	—	inv_eq_of_mul_eq_one_right pow_two_sub_pow_two sq_sqrt sub_nonneg_of_le covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid one_le_pow₀ instZeroLEOneClass IsOrderedRing.toPosMulMono instIsOrderedRing sub_sub_cancel
analyticAt_arcosh 📖	mathematical	Real Set Set.instMembership Set.Ioi instPreorder instOne	AnalyticAt DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField arcosh	—	ContDiffAt.analyticAt contDiffAt_arcosh
analyticOnNhd_arcosh 📖	mathematical	Set Real Set.instHasSubset Set.Ioi instPreorder instOne	AnalyticOnNhd DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField arcosh	—	analyticAt_arcosh
analyticOn_arcosh 📖	mathematical	Set Real Set.instHasSubset Set.Ioi instPreorder instOne	AnalyticOn DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField arcosh	—	AnalyticOn.mono ContDiffOn.analyticOn contDiffOn_arcosh
analyticWithinAt_arcosh 📖	mathematical	Real Set Set.instMembership Set.Ioi instPreorder instOne	AnalyticWithinAt DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField arcosh	—	ContDiffWithinAt.analyticWithinAt ContDiffAt.contDiffWithinAt contDiffAt_arcosh
arcosh_bijOn 📖	mathematical	—	Set.BijOn Real arcosh Set.Ici instPreorder instOne instZero	—	PartialEquiv.bijOn
arcosh_cosh 📖	mathematical	Real instLE instZero	arcosh cosh	—	arcosh.eq_1 exp_eq_exp exp_log add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid cosh_pos sqrt_nonneg eq_sub_iff_add_eq' exp_sub_cosh sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsOrderedRing.toMulPosMono instIsOrderedRing sinh_nonneg_iff sinh_sq sq_sqrt pow_two_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono
arcosh_eq_zero_iff 📖	mathematical	Real instLE instOne	arcosh instZero	—	exp_injective exp_arcosh exp_zero
arcosh_injOn 📖	mathematical	—	Set.InjOn Real arcosh Set.Ici instPreorder instOne	—	PartialEquiv.injOn
arcosh_le_arcosh 📖	mathematical	Real instLT instZero	instLE arcosh	—	StrictMonoOn.le_iff_le strictMonoOn_arcosh
arcosh_lt_arcosh 📖	mathematical	Real instLT instZero	arcosh	—	StrictMonoOn.lt_iff_lt strictMonoOn_arcosh
arcosh_nonneg 📖	mathematical	Real instLE instOne	instZero arcosh	—	log_nonneg add_zero add_le_add_right IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sqrt_nonneg
arcosh_pos 📖	mathematical	Real instLT instOne	instZero arcosh	—	log_pos add_zero add_le_add_right IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sqrt_nonneg
arcosh_surjOn 📖	mathematical	—	Set.SurjOn Real arcosh Set.Ici instPreorder instOne instZero	—	PartialEquiv.surjOn
arcosh_zero 📖	mathematical	—	arcosh Real instOne instZero	—	one_pow sub_self sqrt_zero add_zero log_one
contDiffAt_arcosh 📖	mathematical	Real Set Set.instMembership Set.Ioi instPreorder instOne	ContDiffAt DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField arcosh	—	OpenPartialHomeomorph.contDiffAt_symm_deriv instCompleteSpace sinh_eq_zero LT.lt.ne' arcosh_pos hasDerivAt_cosh ContDiff.contDiffAt contDiff_cosh
contDiffOn_arcosh 📖	mathematical	—	ContDiffOn Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField arcosh Set.Ioi instPreorder instOne	—	ContDiffAt.contDiffWithinAt contDiffAt_arcosh
continuousOn_arcosh 📖	mathematical	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace arcosh Set.Ici instPreorder instOne	—	add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sqrt_nonneg ContinuousOn.comp continuousOn_log Continuous.continuousOn Continuous.fun_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_id' Continuous.comp' continuous_sqrt Continuous.pow IsTopologicalSemiring.toContinuousMul continuous_const
cosh_arcosh 📖	mathematical	Real instLE instOne	cosh arcosh	—	arcosh.eq_1 Nat.instAtLeastTwoHAddOfNat cosh_eq exp_neg exp_log add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one sqrt_nonneg add_sqrt_self_sq_sub_one_inv Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
cosh_bijOn 📖	mathematical	—	Set.BijOn Real cosh Set.Ici instPreorder instZero instOne	—	PartialEquiv.bijOn
cosh_injOn 📖	mathematical	—	Set.InjOn Real cosh Set.Ici instPreorder instZero	—	PartialEquiv.injOn
cosh_surjOn 📖	mathematical	—	Set.SurjOn Real cosh Set.Ici instPreorder instZero instOne	—	PartialEquiv.surjOn
differentiableAt_arcosh 📖	mathematical	Real Set Set.instMembership Set.Ioi instPreorder instOne	DifferentiableAt DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace arcosh	—	HasDerivAt.differentiableAt hasDerivAt_arcosh
differentiableOn_arcosh 📖	mathematical	—	DifferentiableOn Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace arcosh Set.Ioi instPreorder instOne	—	DifferentiableAt.differentiableWithinAt differentiableAt_arcosh
exp_arcosh 📖	mathematical	Real instLE instOne	exp arcosh instAdd sqrt instSub Monoid.toNatPow instMonoid	—	exp_log add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one sqrt_nonneg
hasDerivAt_arcosh 📖	mathematical	Real Set Set.instMembership Set.Ioi instPreorder instOne	HasDerivAt 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 MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal arcosh instInv sqrt instSub Monoid.toNatPow instMonoid	—	HasStrictDerivAt.hasDerivAt hasStrictDerivAt_arcosh
hasStrictDerivAt_arcosh 📖	mathematical	Real Set Set.instMembership Set.Ioi instPreorder instOne	HasStrictDerivAt 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 MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal arcosh instInv sqrt instSub Monoid.toNatPow instMonoid	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal sinh_arcosh le_of_lt OpenPartialHomeomorph.hasStrictDerivAt_symm sinh_eq_zero ne_of_gt arcosh_pos hasStrictDerivAt_cosh
sinh_arcosh 📖	mathematical	Real instLE instOne	sinh arcosh sqrt instSub Monoid.toNatPow instMonoid	—	arcosh.eq_1 Nat.instAtLeastTwoHAddOfNat sinh_eq exp_neg exp_log add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one sqrt_nonneg add_sqrt_self_sq_sub_one_inv Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
strictMonoOn_arcosh 📖	mathematical	—	StrictMonoOn Real instPreorder arcosh Set.Ioi instZero	—	StrictMonoOn.comp strictMonoOn_log StrictMonoOn.add_monotone IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add strictMonoOn_id sqrt_monotone sub_le_sub_right pow_le_pow_left₀ IsOrderedRing.toPosMulMono instIsOrderedRing IsOrderedRing.toMulPosMono le_of_lt add_pos_of_pos_of_nonneg sqrt_nonneg
tanh_arcosh 📖	mathematical	Real instLE instOne	tanh arcosh DivInvMonoid.toDiv instDivInvMonoid sqrt instSub Monoid.toNatPow instMonoid	—	tanh_eq_sinh_div_cosh sinh_arcosh cosh_arcosh

---

← Back to Index