Theorems · Definition · geometry
EuclideanGeometry.Sphere.center
{P : Type u_2} → [inst : MetricSpace P] → EuclideanGeometry.Sphere P → Pcenter of this sphere
- Defined in
- Mathlib.Geometry.Euclidean.Sphere.Basic
- Cited by
- 181 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- MetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MetricSpacestatement and proof · cited by 1,684
- EuclideanGeometry.Spherestatement and proof · cited by 233
Cited by196
Results whose statement or proof uses this declaration.
- Affine.Simplex.excenterproof · cited by 63
- Affine.Simplex.circumcenterproof · cited by 49
- EuclideanGeometry.Sphere.orthRadiusproof · cited by 41
- Affine.Simplex.incenterproof · cited by 35
- EuclideanGeometry.mem_spherestatement · cited by 22
- EuclideanGeometry.Sphere.secondInterproof · cited by 18
- EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_centerstatement · 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.IsDiameter.right_memproof · cited by 7
- EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_leftstatement and proof · cited by 7