Theorems · Definition · geometry
EuclideanGeometry.Sphere.radius
{P : Type u_2} → [inst : MetricSpace P] → EuclideanGeometry.Sphere P → ℝradius of the sphere; not required to be positive
- Defined in
- Mathlib.Geometry.Euclidean.Sphere.Basic
- Cited by
- 123 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 4 definitions · uses no axioms
- Assumes
- MetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- MetricSpacestatement and proof · cited by 1,684
- EuclideanGeometry.Spherestatement and proof · cited by 233
Cited by128
Results whose statement or proof uses this declaration.
- Affine.Simplex.circumradiusproof · cited by 35
- EuclideanGeometry.mem_spherestatement · cited by 22
- Affine.Simplex.exradiusproof · cited by 18
- Affine.Simplex.inradiusproof · cited by 11
- EuclideanGeometry.Sphere.powerproof · cited by 11
- EuclideanGeometry.mem_sphere'statement · cited by 10
- EuclideanGeometry.Sphere.extstatement and proof · cited by 10
- EuclideanGeometry.Sphere.radius_nonneg_of_memstatement · cited by 9
- Affine.Simplex.circumsphere_unique_dist_eqstatement · cited by 6
- EuclideanGeometry.Sphere.IsTangentAt.dist_sq_eq_of_memstatement · cited by 6
- EuclideanGeometry.Sphere.tangentSetproof · cited by 6
- Affine.Simplex.eq_circumcenter_of_dist_eqproof · cited by 5