Theorems · Theorem · functional analysis
NormedSpace.sphere_nonempty
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E] {x : E} {r : ℝ},
(Metric.sphere x r).Nonempty ↔ 0 ≤ rIn a nontrivial real normed space, a sphere is nonempty if and only if its radius is nonnegative.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- NormedSpacestatement and proof · cited by 12,499
- Norm.normproof · cited by 5,413
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- Set.Nonemptystatement and proof · cited by 2,627
- Metric.spherestatement and proof · cited by 371
- add_sub_cancel_leftproof · cited by 198
- Set.Nonempty.monoproof · cited by 88
- NontrivialTopologystatement and proof · cited by 46
- Metric.sphere_subset_closedBallproof · cited by 24
- Metric.nonempty_closedBallproof · cited by 13
- exists_norm_eqproof · cited by 4
Cited by8
Results whose statement or proof uses this declaration.
- AnalyticAt.eventually_constant_or_nhds_le_map_nhds_auxproof · cited by 1
- convexHull_sphere_eq_closedBallproof · cited by 1
- ContinuousLinearMap.sSup_sphere_eq_nnnormproof · cited by 1
- Complex.norm_cderiv_leproof · cited by 1
- Complex.norm_cderiv_ltproof · cited by 1
- EuclideanGeometry.Sphere.nonempty_iffproof · cited by 1
- Complex.circleTransformDeriv_boundproof · cited by 0
- NormedSpace.sphere_nonempty_rclikeproof · cited by 0