Mathlib Map

Theorems · Theorem · real analysis

Real.strictMonoOn_artanh

StrictMonoOn Real.artanh (Set.Ioo (-1) 1)
Defined in
Mathlib.Analysis.SpecialFunctions.Artanh
Cited by
2 results in Mathlib
Foundations
Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Real.artanh_le_artanh_iff · cited by 3Real.artanh_le_artanh_iffReal.artanh_lt_artanh_iff · cited by 3Real.artanh_lt_artanh_iffReal · cited by 25697RealSet.Ioo · cited by 1214Set.Ioodiv_pos · cited by 337div_posStrictMonoOn · cited by 194StrictMonoOndiv_nonneg · cited by 103div_nonnegReal.sqrt_pos_of_pos · cited by 50Real.sqrt_pos_of_posReal.artanh · cited by 20Real.artanhReal.strictMonoOn_log · cited by 13Real.strictMonoOn_logStrictMonoOn.comp · cited by 2StrictMonoOn.compReal.strictMonoOn_one_add_div_one_sub · cited by 1Real.strictMonoOn_one_add…Real.strictMonoOn_sqrt · cited by 1Real.strictMonoOn_sqrtReal.strictMonoOn_artanhCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.