EuclideanGeometry.dist_of_mem_subset_sphere
∀ {P : Type u_2} [inst : MetricSpace P] {p : P} {ps : Set P} {s : EuclideanGeometry.Sphere P},
p ∈ ps → ps ⊆ Metric.sphere s.center s.radius → dist p s.center = s.radius- Defined in
- Mathlib.Geometry.Euclidean.Sphere.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- MetricSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Realstatement · cited by 25,697
- MetricSpacestatement and proof · cited by 1,684
- Dist.diststatement · cited by 1,539
- Metric.spherestatement and proof · cited by 371
- EuclideanGeometry.Spherestatement and proof · cited by 233
- EuclideanGeometry.Sphere.centerstatement and proof · cited by 181
- EuclideanGeometry.Sphere.radiusstatement and proof · cited by 123
- Set.mem_of_mem_of_subsetproof · cited by 36
- EuclideanGeometry.mem_sphereproof · cited by 22
- EuclideanGeometry.Sphere.mem_coeproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- Affine.Simplex.dist_circumcenter_eq_circumradiusproof · cited by 12
- EuclideanGeometry.dist_of_mem_subset_mk_sphereproof · cited by 1