Theorems · Theorem · general topology
Metric.mem_eball
∀ {α : Type u} [inst : EDist α] {x y : α} {ε : ENNReal}, y ∈ Metric.eball x ε ↔ edist y x < ε- Defined in
- Mathlib.Topology.EMetricSpace.Defs
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 111 from the axioms · 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
- EDist.ediststatement · cited by 735
- Metric.eballstatement · cited by 294
- EDiststatement and proof · cited by 91
Cited by18
Results whose statement or proof uses this declaration.
- mem_eball_zero_iffproof · cited by 8
- Metric.mem_eball_selfproof · cited by 6
- Metric.mem_eball'proof · cited by 3
- HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principalproof · cited by 3
- setOfPred_riemannianEDist_lt_subset_nhdsproof · cited by 2
- HasFiniteFPowerSeriesOnBall.eq_partialSum'proof · cited by 2
- HasFPowerSeriesWithinOnBall.prodproof · cited by 2
- Metric.exists_eball_subset_eballproof · cited by 2
- HasFPowerSeriesWithinAt.compproof · cited by 2
- Metric.mem_eball_commproof · cited by 1
- mem_eball_one_iffproof · cited by 1
- Complex.hasSum_taylorSeries_of_entireproof · cited by 1