Theorems · Theorem · special functions
Polynomial.Chebyshev.intervalIntegrable_sqrt_one_sub_sq_inv
IntervalIntegrable (fun x => √(1 - x ^ 2)⁻¹) MeasureTheory.volume (-1) 1
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 266 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MeasureTheory.MeasureSpace.volumestatement · cited by 1,323
- Set.Iooproof · cited by 1,214
- neg_negproof · cited by 960
- one_divproof · cited by 624
- Real.sqrtstatement and proof · cited by 545
- IntervalIntegrablestatement · cited by 316
- Continuous.continuousOnproof · cited by 311
- inf_of_le_leftproof · cited by 186
- sup_of_le_rightproof · cited by 143
- Real.arccosproof · cited by 90
- HasDerivAt.congr_simpproof · cited by 82
Cited by1
Results whose statement or proof uses this declaration.
- Polynomial.Chebyshev.integrable_measureTproof · cited by 2