Theorems · Theorem · real analysis
Real.range_arctan
Set.range Real.arctan = Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement · cited by 25,697
- Set.rangestatement · cited by 4,705
- Real.pistatement · cited by 1,774
- Set.Ioostatement · cited by 1,214
- OrderIso.symmproof · cited by 475
- Real.arctanstatement · cited by 111
- Subtype.range_coeproof · cited by 98
- EquivLike.surjectiveproof · cited by 24
- Function.Surjective.range_compproof · cited by 18
- Real.tanOrderIsoproof · cited by 10
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.