Mathlib Map

Theorems · Theorem · general topology

Real.dist_eq

∀ (x y : ℝ), dist x y = |x - y|
Defined in
Mathlib.Topology.MetricSpace.Pseudo.Defs
Cited by
27 results in Mathlib
Foundations
Depth 114 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.

Real.closedBall_eq_Icc · cited by 13Real.closedBall_eq_IccReal.ball_eq_Ioo · cited by 11Real.ball_eq_IooMonotoneOn.eVariationOn_eq · cited by 4MonotoneOn.eVariationOn_eqComplex.dist_of_re_eq · cited by 4Complex.dist_of_re_eqCircleDeg1Lift.dist_map_map_zero_lt · cited by 3CircleDeg1Lift.dist_map_m…PhragmenLindelof.horizontal_strip · cited by 3PhragmenLindelof.horizont…Real.sub_le_dist · cited by 2Real.sub_le_distUpperHalfPlane.dist_of_re_eq · cited by 2UpperHalfPlane.dist_of_re…UpperHalfPlane.dist_self_center · cited by 2UpperHalfPlane.dist_self_…CircleDeg1Lift.tendsto_translationNumber_of_dist_bounded_aux · cited by 2CircleDeg1Lift.tendsto_tr…variationOnFromTo.abs_sub_le_sub_of_le · cited by 2variationOnFromTo.abs_sub…Complex.dist_conj_self · cited by 2Complex.dist_conj_selfAbsolutelyContinuousOnInterval.boundedVariationOn · cited by 2AbsolutelyContinuousOnInt…IsMIntegralCurveAt.comp_mul_ne_zero · cited by 1IsMIntegralCurveAt.comp_m…MeasureTheory.lintegral_abs_det_fderiv_le_addHaar_image_aux1 · cited by 1MeasureTheory.lintegral_a…Real · cited by 25697Realabs · cited by 1814absDist.dist · cited by 1539Dist.distReal.dist_eqCITED BYCITES

Cites3

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
  • absstatement · cited by 1,814
  • Dist.diststatement · cited by 1,539

Cited by27

Results whose statement or proof uses this declaration.