Theorems · Theorem · general topology
edist_ne_top
∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), edist x y ≠ ⊤In a pseudometric space, the extended distance is always finite
- Defined in
- Mathlib.Topology.MetricSpace.Pseudo.Defs
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- PseudoMetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement · cited by 9,879
- Top.topstatement · cited by 9,680
- PseudoMetricSpacestatement and proof · cited by 1,550
- LT.lt.neproof · cited by 872
- EDist.ediststatement · cited by 735
- edist_lt_topproof · cited by 32
Cited by17
Results whose statement or proof uses this declaration.
- Metric.infDist_le_dist_of_memproof · cited by 13
- Metric.infEDist_ne_topproof · cited by 8
- Metric.mem_thickening_iffproof · cited by 6
- Metric.infDist_eq_iInfproof · cited by 4
- Metric.le_infDistproof · cited by 3
- Metric.infDist_le_infDist_add_distproof · cited by 2
- Set.subsingleton_of_einfsep_eq_topproof · cited by 2
- ContractingWith.fixedPoint_unique'proof · cited by 1
- Real.dist_mulExpNegMulSq_le_distproof · cited by 1
- Dilation.ratio_unique_of_nndist_ne_zeroproof · cited by 1
- ContractingWith.tendsto_iterate_fixedPointproof · cited by 1
- Metric.lipschitz_infDist_setproof · cited by 1