Theorems · Theorem · general topology
Metric.ball_eq_empty
∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.ball x ε = ∅ ↔ ε ≤ 0- Defined in
- Mathlib.Topology.MetricSpace.Pseudo.Defs
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 114 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.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- PseudoMetricSpacestatement and proof · cited by 1,550
- Metric.ballstatement · cited by 735
- not_ltproof · cited by 306
- Set.not_nonempty_iff_eq_emptyproof · cited by 56
- Metric.nonempty_ballproof · cited by 13
Cited by16
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.addHaar_closedBall_eq_addHaar_ballproof · cited by 9
- interior_closedBallproof · cited by 8
- Metric.ball_zeroproof · cited by 5
- InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eqproof · cited by 4
- circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countableproof · cited by 2
- AddCircle.closedBall_ae_eq_ballproof · cited by 2
- EuclideanSpace.volume_ballproof · cited by 2
- uniformCauchySeqOn_ball_of_fderivproof · cited by 2
- DiffContOnCl.circleAverage_re_herglotzRieszKernel_smulproof · cited by 2
- DiffContOnCl.circleAverage_smul_divproof · cited by 2
- DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smulproof · cited by 1
- MeromorphicOn.exists_canonicalDecompproof · cited by 1