Artanh

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

Statistics

Metric	Count
Definitions artanh, tanhPartialEquiv	2
Theorems artanh_bijOn, artanh_eq_half_log, artanh_eq_zero_iff, artanh_injOn, artanh_le_artanh, artanh_le_artanh_iff, artanh_lt_artanh, artanh_lt_artanh_iff, artanh_neg, artanh_nonneg, artanh_nonpos, artanh_pos, artanh_surjOn, artanh_tanh, artanh_zero, cosh_artanh, exp_artanh, sinh_artanh, strictMonoOn_artanh, strictMonoOn_one_add_div_one_sub, tanh_artanh, tanh_bijOn, tanh_injective, tanh_surjOn	24
Total	26

Real

Definitions

Name	Category	Theorems
artanh 📖	CompOp	20 math math: artanh_pos, artanh_nonneg, artanh_bijOn, artanh_zero, strictMonoOn_artanh, artanh_eq_half_log, artanh_surjOn, artanh_le_artanh_iff, artanh_eq_zero_iff, artanh_lt_artanh_iff, artanh_nonpos, tanh_artanh, artanh_le_artanh, artanh_neg, exp_artanh, artanh_lt_artanh, artanh_injOn, sinh_artanh, cosh_artanh, artanh_tanh
tanhPartialEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
artanh_bijOn 📖	mathematical	—	Set.BijOn Real artanh Set.Ioo instPreorder instNeg instOne Set.univ	—	PartialEquiv.bijOn
artanh_eq_half_log 📖	mathematical	Real Set Set.instMembership Set.Icc instPreorder instNeg instOne	artanh instMul DivInvMonoid.toDiv instDivInvMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat log instAdd instSub	—	Nat.instAtLeastTwoHAddOfNat artanh.eq_1 log_sqrt div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing one_div_mul_eq_div
artanh_eq_zero_iff 📖	mathematical	—	artanh Real instZero instLE instNeg instOne	—	—
artanh_injOn 📖	mathematical	—	Set.InjOn Real artanh Set.Ioo instPreorder instNeg instOne	—	PartialEquiv.injOn
artanh_le_artanh 📖	mathematical	Real instLT instNeg instOne instLE	artanh	—	artanh_le_artanh_iff
artanh_le_artanh_iff 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instNeg instOne	instLE artanh	—	StrictMonoOn.le_iff_le strictMonoOn_artanh
artanh_lt_artanh 📖	mathematical	Real instLT instNeg instOne	artanh	—	artanh_lt_artanh_iff
artanh_lt_artanh_iff 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instNeg instOne	instLT artanh	—	StrictMonoOn.lt_iff_lt strictMonoOn_artanh
artanh_neg 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instNeg instOne instZero	instLT artanh	—	artanh_zero artanh_lt_artanh_iff
artanh_nonneg 📖	mathematical	Real instLE instZero	artanh	—	artanh_zero artanh_le_artanh_iff
artanh_nonpos 📖	mathematical	Real instLE instZero	artanh	—	artanh_zero artanh_le_artanh_iff
artanh_pos 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instZero instOne	instLT artanh	—	artanh_zero artanh_lt_artanh_iff
artanh_surjOn 📖	mathematical	—	Set.SurjOn Real artanh Set.Ioo instPreorder instNeg instOne Set.univ	—	PartialEquiv.surjOn
artanh_tanh 📖	mathematical	—	artanh tanh	—	div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing artanh.eq_1 exp_eq_exp exp_log sqrt_pos_of_pos sq_eq_sq₀ IsOrderedRing.toMulPosMono instIsOrderedRing le_of_lt exp_nonneg sq_sqrt tanh_eq exp_neg Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt add_pos' IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid pow_pos IsStrictOrderedRing.toZeroLEOneClass exp_pos Mathlib.Meta.Positivity.pos_of_isNat instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.NF.pow_eq_eval add_sub_sub_cancel NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike NeZero.charZero_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add 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_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add 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_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_overlap_pf_zero
artanh_zero 📖	mathematical	—	artanh Real instZero	—	add_zero sub_zero div_self NeZero.charZero_one RCLike.charZero_rclike sqrt_one log_one
cosh_artanh 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instNeg instOne	cosh artanh DivInvMonoid.toDiv instDivInvMonoid sqrt instSub Monoid.toNatPow instMonoid	—	sqrt_pos_of_pos div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing one_pow sq_sub_sq sqrt_mul
exp_artanh 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instNeg instOne	exp artanh sqrt DivInvMonoid.toDiv instDivInvMonoid instAdd instSub	—	exp_log sqrt_pos_of_pos div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing
sinh_artanh 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instNeg instOne	sinh artanh DivInvMonoid.toDiv instDivInvMonoid sqrt instSub Monoid.toNatPow instMonoid	—	sqrt_pos_of_pos div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing one_pow sq_sub_sq sqrt_mul
strictMonoOn_artanh 📖	mathematical	—	StrictMonoOn Real instPreorder artanh Set.Ioo instNeg instOne	—	StrictMonoOn.comp strictMonoOn_log strictMonoOn_sqrt strictMonoOn_one_add_div_one_sub div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing sqrt_pos_of_pos div_pos
strictMonoOn_one_add_div_one_sub 📖	mathematical	—	StrictMonoOn Real instPreorder DivInvMonoid.toDiv instDivInvMonoid instAdd instOne instSub Set.Ioo instNeg	—	Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_pos instZeroLEOneClass zero_lt_one NeZero.one GroupWithZero.toNontrivial
tanh_artanh 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instNeg instOne	tanh artanh	—	sq_sub_sq
tanh_bijOn 📖	mathematical	—	Set.BijOn Real tanh Set.univ Set.Ioo instPreorder instNeg instOne	—	PartialEquiv.bijOn
tanh_injective 📖	mathematical	—	Real tanh	—	PartialEquiv.injOn
tanh_surjOn 📖	mathematical	—	Set.SurjOn Real tanh Set.univ Set.Ioo instPreorder instNeg instOne	—	PartialEquiv.surjOn

---

← Back to Index