Mathlib Map

Theorems · Theorem · general topology

Dist.ext

∀ {α : Type u_3} {x y : Dist α}, dist = dist → x = y
Defined in
Mathlib.Topology.MetricSpace.Pseudo.Defs
Cited by
9 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

PseudoMetricSpace.replaceTopology_eq · cited by 1PseudoMetricSpace.replace…MetricSpace.replaceTopology_eq · cited by 1MetricSpace.replaceTopolo…PseudoMetricSpace.replaceBornology_eq · cited by 0PseudoMetricSpace.replace…PseudoMetricSpace.replaceDist_eq · cited by 0PseudoMetricSpace.replace…PseudoMetricSpace.replaceUniformity_eq · cited by 0PseudoMetricSpace.replace…Dist.ext_iff · cited by 0Dist.ext_iffMetricSpace.replaceBornology_eq · cited by 0MetricSpace.replaceBornol…MetricSpace.replaceDist_eq · cited by 0MetricSpace.replaceDist_eqMetricSpace.replaceUniformity_eq · cited by 0MetricSpace.replaceUnifor…Real · cited by 25697RealDist.dist · cited by 1539Dist.distDist · cited by 35DistDist.extCITED 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
  • Dist.diststatement and proof · cited by 1,539
  • Diststatement and proof · cited by 35

Cited by9

Results whose statement or proof uses this declaration.