Theorems · Definition · real analysis
Real.sinOrderIso
↑(Set.Icc (-(Real.pi / 2)) (Real.pi / 2)) ≃o ↑(Set.Icc (-1) 1)
Real.sin as an OrderIso between [-(π / 2), π / 2] and [-1, 1].
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 185 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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.Elemstatement · cited by 7,166
- Set.imageproof · cited by 5,609
- Real.pistatement and proof · cited by 1,774
- Set.Iccstatement and proof · cited by 1,702
- OrderIsostatement · cited by 874
- Real.sinproof · cited by 389
- OrderIso.transproof · cited by 31
- OrderIso.setCongrproof · cited by 10
- Real.strictMonoOn_sinproof · cited by 4
- StrictMonoOn.orderIsoproof · cited by 2
Cited by10
Results whose statement or proof uses this declaration.
- Real.arcsinproof · cited by 125
- Real.continuous_arcsinproof · cited by 8
- Real.arcsin_mem_Iccproof · cited by 4
- Real.strictMonoOn_arcsinproof · cited by 4
- Real.sin_arcsin'proof · cited by 3
- Real.arcsin_projIccproof · cited by 2
- Real.monotone_arcsinproof · cited by 2
- Real.sinOrderIso_applystatement · cited by 0
- Real.range_arcsinproof · cited by 0
- Real.coe_sinOrderIso_applystatement · cited by 0