Mathlib Map

Theorems · Definition · real analysis

EReal.abs

EReal → ENNReal

The absolute value from EReal to ℝ≥0∞, mapping ⊥ and ⊤ to ⊤ and a real x to |x|.

Defined in
Mathlib.Data.EReal.Inv
Cited by
15 results in Mathlib
Foundations
Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

EReal.abs_def · cited by 4EReal.abs_defEReal.abs_zero · cited by 3EReal.abs_zeroEReal.sign_mul_abs · cited by 3EReal.sign_mul_absEReal.abs_eq_zero_iff · cited by 2EReal.abs_eq_zero_iffEReal.abs_neg · cited by 1EReal.abs_negEReal.abs_top · cited by 1EReal.abs_topEReal.coe_abs · cited by 1EReal.coe_absEReal.abs_bot · cited by 0EReal.abs_botEReal.abs_coe_lt_top · cited by 0EReal.abs_coe_lt_topEReal.abs_mul · cited by 0EReal.abs_mulEReal.abs_mul_sign · cited by 0EReal.abs_mul_signEReal.le_iff_sign · cited by 0EReal.le_iff_signEReal.sign_eq_and_abs_eq_iff_eq · cited by 0EReal.sign_eq_and_abs_eq_…EReal.sign_mul_inv_abs · cited by 0EReal.sign_mul_inv_absEReal.sign_mul_inv_abs' · cited by 0EReal.sign_mul_inv_abs'Real · cited by 25697RealENNReal · cited by 9879ENNRealTop.top · cited by 9680Top.topabs · cited by 1814absENNReal.ofReal · cited by 863ENNReal.ofRealEReal · cited by 793ERealEReal.absCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Realproof · cited by 25,697
  • ENNRealstatement and proof · cited by 9,879
  • Top.topproof · cited by 9,680
  • absproof · cited by 1,814
  • ENNReal.ofRealproof · cited by 863
  • ERealstatement and proof · cited by 793

Cited by15

Results whose statement or proof uses this declaration.