Theorems · Theorem · geometry

EuclideanGeometry.Sphere.IsTangent.infDist_eq_radius

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P},
  s.IsTangent as → Metric.infDist s.center ↑as = s.radius

Defined in: Mathlib.Geometry.Euclidean.Sphere.Tangent
Cited by: 2 results in Mathlib
Foundations: Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup InnerProductSpace MetricSpace NormedAddTorsor

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites25

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
NormedAddCommGroupstatement and proof · cited by 15,752
SetLike.coestatement and proof · cited by 8,199
Set.Elemproof · cited by 7,166
InnerProductSpacestatement and proof · cited by 3,523
le_antisymmproof · cited by 2,068
MetricSpacestatement and proof · cited by 1,684
Dist.distproof · cited by 1,539
NormedAddTorsorstatement and proof · cited by 1,325
AffineSubspacestatement and proof · cited by 871
EuclideanGeometry.Spherestatement and proof · cited by 233
dist_commproof · cited by 188

Cited by2

Results whose statement or proof uses this declaration.

EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAtproof · cited by 3
EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentproof · cited by 2