Commit 2025-03-31 15:58 e0971f3d

View on Github →

feat(Geometry/Euclidean/Sphere/Tangent): tangents to spheres (#22483) Add various basic definitions and lemmas relating to spheres being tangent to affine subspaces and other spheres. (Material involving angles, such as the alternate segment theorem, is expected to be added separately in followups.)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Euclidean/Sphere/Tangent.lean

added theorem EuclideanGeometry.Sphere.IsExtTangent.dist_center

added theorem EuclideanGeometry.Sphere.IsExtTangent.symm

added def EuclideanGeometry.Sphere.IsExtTangent

added theorem EuclideanGeometry.Sphere.IsExtTangentAt.isExtTangent

added theorem EuclideanGeometry.Sphere.IsExtTangentAt.symm

added structure EuclideanGeometry.Sphere.IsExtTangentAt

added theorem EuclideanGeometry.Sphere.IsIntTangent.dist_center

added def EuclideanGeometry.Sphere.IsIntTangent

added theorem EuclideanGeometry.Sphere.IsIntTangentAt.isIntTangent

added structure EuclideanGeometry.Sphere.IsIntTangentAt

added def EuclideanGeometry.Sphere.IsTangent

added theorem EuclideanGeometry.Sphere.IsTangentAt.eq_of_isTangentAt

added theorem EuclideanGeometry.Sphere.IsTangentAt.inner_left_eq_zero_of_mem

added theorem EuclideanGeometry.Sphere.IsTangentAt.inner_right_eq_zero_of_mem

added theorem EuclideanGeometry.Sphere.IsTangentAt.isTangent

added structure EuclideanGeometry.Sphere.IsTangentAt

added theorem EuclideanGeometry.Sphere.center_mem_orthRadius_iff

added def EuclideanGeometry.Sphere.commonExtTangents

added def EuclideanGeometry.Sphere.commonIntTangents

added theorem EuclideanGeometry.Sphere.commonIntTangents_union_commonExtTangents

added def EuclideanGeometry.Sphere.commonTangents

added theorem EuclideanGeometry.Sphere.commonTangents_comm

added theorem EuclideanGeometry.Sphere.direction_orthRadius

added theorem EuclideanGeometry.Sphere.isExtTangentAt_center_iff

added theorem EuclideanGeometry.Sphere.isExtTangentAt_comm

added theorem EuclideanGeometry.Sphere.isExtTangent_comm

added theorem EuclideanGeometry.Sphere.isExtTangent_iff_dist_center

added theorem EuclideanGeometry.Sphere.isIntTangentAt_center_iff

added theorem EuclideanGeometry.Sphere.isIntTangentAt_self_iff_mem

added theorem EuclideanGeometry.Sphere.isIntTangent_iff_dist_center

added theorem EuclideanGeometry.Sphere.isIntTangent_self_iff

added theorem EuclideanGeometry.Sphere.isTangentAt_center_iff

added theorem EuclideanGeometry.Sphere.isTangentAt_orthRadius_iff_mem

added theorem EuclideanGeometry.Sphere.isTangent_of_mem_tangentSet

added theorem EuclideanGeometry.Sphere.isTangent_of_mem_tangentsFrom

added theorem EuclideanGeometry.Sphere.isTangent_orthRadius_iff_mem

added theorem EuclideanGeometry.Sphere.mem_commonExtTangents_iff

added theorem EuclideanGeometry.Sphere.mem_commonIntTangents_iff

added theorem EuclideanGeometry.Sphere.mem_commonTangents_iff

added theorem EuclideanGeometry.Sphere.mem_of_mem_tangentsFrom

added theorem EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left

added theorem EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_right

added theorem EuclideanGeometry.Sphere.mem_tangentSet_iff

added theorem EuclideanGeometry.Sphere.mem_tangentSet_of_mem_tangentsFrom

added theorem EuclideanGeometry.Sphere.mem_tangentsFrom_iff

added def EuclideanGeometry.Sphere.orthRadius

added theorem EuclideanGeometry.Sphere.orthRadius_center

added theorem EuclideanGeometry.Sphere.orthRadius_eq_orthRadius_iff

added theorem EuclideanGeometry.Sphere.orthRadius_le_orthRadius_iff

added theorem EuclideanGeometry.Sphere.self_mem_orthRadius

added def EuclideanGeometry.Sphere.tangentSet

added def EuclideanGeometry.Sphere.tangentsFrom