Theorems · Definition · general topology
ENNReal.powOrderIso
(n : ℕ) → n ≠ 0 → ENNReal ≃o ENNReal
x ↦ x ^ n as an order isomorphism of ℝ≥0∞.
See also ENNReal.orderIsoRpow.
- Defined in
- Mathlib.Topology.Instances.NNReal.Lemmas
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- ENNRealstatement · cited by 9,879
- NNRealproof · cited by 4,310
- WithTopproof · cited by 3,754
- OrderIsostatement · cited by 874
- RelIso.symmproof · cited by 193
- OrderIso.withTopCongrproof · cited by 6
- RelIso.copyproof · cited by 2
- NNReal.powOrderIsoproof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- ENNReal.iSup_pow_of_ne_zeroproof · cited by 1
- ENNReal.iSup₂_pow_of_ne_zeroproof · cited by 1