Commit 2026-03-27 17:02 02b1b6c9

View on Github →

feat(Geometry/Euclidean/Sphere/OrthRadius): lemmas for setting up and using polars (#31891) Add further lemmas about orthRadius that are of use in setting up and using poles and polars. In particular, ncard_inter_orthRadius_eq_two_of_dist_lt_radius is the key part of showing that, in two dimensions, there are exactly two tangents to a circle from a point outside that circle (where the points of tangency lie on the polar of the point from which the two tangents are drawn).

Estimated changes

Modified Mathlib/Geometry/Euclidean/Sphere/OrthRadius.lean

added theorem EuclideanGeometry.Sphere.dist_sq_eq_iff_mem_orthRadius

added theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_iff

added theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_of_finrank_eq_one

added theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_empty_of_radius_lt_dist

added theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_of_dist_le_radius

added theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_of_dist_le_radius_of_norm_eq_one

added theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_singleton_iff

added theorem EuclideanGeometry.Sphere.inter_orthRadius_eq_singleton_of_dist_eq_radius

added theorem EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq

added theorem EuclideanGeometry.Sphere.mem_inter_orthRadius_iff_vsub_mem_and_norm_sq

added theorem EuclideanGeometry.Sphere.ncard_inter_orthRadius_eq_two_of_dist_lt_radius

added theorem EuclideanGeometry.Sphere.ncard_inter_orthRadius_le_two

added theorem EuclideanGeometry.Sphere.orthRadius_injective

added theorem EuclideanGeometry.Sphere.orthogonalProjection_orthRadius_center

modified theorem EuclideanGeometry.Sphere.self_mem_orthRadius

added theorem EuclideanGeometry.Sphere.vadd_mem_inter_orthRadius_iff_norm_sq

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