Theorems · Theorem · geometry

EuclideanGeometry.Sphere.IsTangentAt.isTangent

∀ {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} {p : P} {as : AffineSubspace ℝ P},
  s.IsTangentAt p as → s.IsTangent as

Defined in: Mathlib.Geometry.Euclidean.Sphere.Tangent
Cited by: 7 results in Mathlib
Foundations: Depth 164 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.

Cites9

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
InnerProductSpacestatement and proof · cited by 3,523
MetricSpacestatement and proof · cited by 1,684
NormedAddTorsorstatement and proof · cited by 1,325
AffineSubspacestatement and proof · cited by 871
EuclideanGeometry.Spherestatement and proof · cited by 233
EuclideanGeometry.Sphere.IsTangentAtstatement and proof · cited by 35
EuclideanGeometry.Sphere.IsTangentstatement · cited by 13

Cited by7

Results whose statement or proof uses this declaration.

EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAtproof · cited by 3
EuclideanGeometry.Sphere.IsTangent.infDist_eq_radiusproof · cited by 2
EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentproof · cited by 2
Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpointproof · cited by 2
EuclideanGeometry.Sphere.isTangent_orthRadius_iff_memproof · cited by 1
EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjectionproof · cited by 1
EuclideanGeometry.Sphere.dist_sq_eq_mul_dist_of_tangent_and_secantproof · cited by 0