Theorems · Definition · general topology
Metric.eball
{α : Type u} → [EDist α] → α → ENNReal → Set αEMetric.ball x ε is the set of all points y with edist y x < ε
- Defined in
- Mathlib.Topology.EMetricSpace.Defs
- Cited by
- 294 results in Mathlib
- Foundations
- Depth 110 from the axioms, rests on 2,020 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- EDist
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- ENNRealstatement and proof · cited by 9,879
- Set.ofPredproof · cited by 6,101
- EDist.edistproof · cited by 735
- EDiststatement and proof · cited by 91
Cited by306
Results whose statement or proof uses this declaration.
- HasFPowerSeriesWithinOnBall.hasSumstatement · cited by 28
- Metric.eball_mem_nhdsstatement · cited by 25
- HasFPowerSeriesOnBall.hasSumstatement · cited by 24
- Metric.mem_eballstatement · cited by 18
- hasFPowerSeriesWithinOnBall_univproof · cited by 16
- Metric.eball_subset_eballstatement · cited by 14
- Metric.isOpen_eballstatement · cited by 13
- Metric.eball_coestatement and proof · cited by 13
- Metric.nhds_basis_eballstatement · cited by 10
- HasFPowerSeriesOnBall.monoproof · cited by 10
- HasFPowerSeriesOnBall.congrstatement and proof · cited by 9
- mem_eball_zero_iffstatement · cited by 8
Showing the 200 most cited of 306.