Theorems · Theorem · general topology
continuous_edist
∀ {α : Type u_1} [inst : PseudoEMetricSpace α], Continuous fun p => edist p.1 p.2- Cited by
- 9 results in Mathlib
- Foundations
- Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PseudoEMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- Continuousstatement · cited by 2,592
- mul_commproof · cited by 2,262
- le_reflproof · cited by 2,061
- PseudoEMetricSpacestatement and proof · cited by 1,536
- EDist.ediststatement and proof · cited by 735
- add_le_addproof · cited by 666
- le_max_leftproof · cited by 215
- le_max_rightproof · cited by 205
- PseudoEMetricSpace.edist_commproof · cited by 52
- mul_twoproof · cited by 43
- continuous_of_le_add_edistproof · cited by 4
Cited by9
Results whose statement or proof uses this declaration.
- Continuous.edistproof · cited by 7
- Metric.ediam_closureproof · cited by 5
- MeasureTheory.StronglyMeasurable.edistproof · cited by 3
- Filter.Tendsto.edistproof · cited by 3
- ProbabilityTheory.IsKolmogorovProcess.stronglyMeasurable_edistproof · cited by 2
- MeasureTheory.AEStronglyMeasurable.edistproof · cited by 1
- measurable_edistproof · cited by 0
- AEMeasurable.edistproof · cited by 0
- Measurable.edistproof · cited by 0