Theorems · Definition · real analysis
Real.nnabs
ℝ →*₀ NNReal
The absolute value on ℝ as a map to ℝ≥0.
- Defined in
- Mathlib.Data.NNReal.Defs
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- NNRealstatement · cited by 4,310
- absproof · cited by 1,814
- MonoidWithZeroHomstatement · cited by 704
Cited by27
Results whose statement or proof uses this declaration.
- Real.coe_nnabsstatement · cited by 6
- Real.nnabs_of_nonnegstatement and proof · cited by 6
- hasFDerivAt_integral_of_dominated_of_fderiv_leproof · cited by 5
- hasFDerivAt_integral_of_dominated_loc_of_lipstatement and proof · cited by 4
- hasDerivAt_integral_of_dominated_loc_of_deriv_leproof · cited by 4
- Real.nndist_eq'statement · cited by 3
- hasDerivAt_integral_of_dominated_loc_of_lipstatement and proof · cited by 2
- BoxIntegral.Box.distortion_eq_of_sub_eq_divproof · cited by 1
- EReal.coe_absproof · cited by 1
- Complex.nndist_conj_selfstatement and proof · cited by 1
- ENNReal.exists_frequently_lt_of_liminf_ne_topstatement and proof · cited by 1
- ENNReal.exists_frequently_lt_of_liminf_ne_top'statement and proof · cited by 1