Commit 2023-06-14 13:55 6b93a4a3

View on Github →

feat: port Geometry.Euclidean.Circumcenter (#4446)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Basic.lean

Created Mathlib/Geometry/Euclidean/Circumcenter.lean

added inductive Affine.Simplex.PointsWithCircumcenterIndex

added def Affine.Simplex.centroidWeightsWithCircumcenter

added theorem Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter

added def Affine.Simplex.circumcenter

added def Affine.Simplex.circumcenterWeightsWithCircumcenter

added theorem Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter

added theorem Affine.Simplex.circumcenter_eq_centroid

added theorem Affine.Simplex.circumcenter_eq_of_range_eq

added theorem Affine.Simplex.circumcenter_eq_point

added theorem Affine.Simplex.circumcenter_mem_affineSpan

added theorem Affine.Simplex.circumcenter_reindex

added def Affine.Simplex.circumradius

added theorem Affine.Simplex.circumradius_nonneg

added theorem Affine.Simplex.circumradius_pos

added theorem Affine.Simplex.circumradius_reindex

added def Affine.Simplex.circumsphere

added theorem Affine.Simplex.circumsphere_center

added theorem Affine.Simplex.circumsphere_radius

added theorem Affine.Simplex.circumsphere_reindex

added theorem Affine.Simplex.circumsphere_unique_dist_eq

added theorem Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection

added theorem Affine.Simplex.dist_circumcenter_eq_circumradius'

added theorem Affine.Simplex.dist_circumcenter_eq_circumradius

added theorem Affine.Simplex.dist_circumcenter_sq_eq_sq_sub_circumradius

added theorem Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq

added theorem Affine.Simplex.eq_circumcenter_of_dist_eq

added theorem Affine.Simplex.eq_circumradius_of_dist_eq

added theorem Affine.Simplex.mem_circumsphere

added def Affine.Simplex.orthogonalProjectionSpan

added theorem Affine.Simplex.orthogonalProjection_circumcenter

added theorem Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq

added theorem Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq

added theorem Affine.Simplex.orthogonalProjection_vadd_smul_vsub_orthogonalProjection

added def Affine.Simplex.pointIndexEmbedding

added def Affine.Simplex.pointWeightsWithCircumcenter

added theorem Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenter

added def Affine.Simplex.pointsWithCircumcenter

added theorem Affine.Simplex.pointsWithCircumcenter_eq_circumcenter

added theorem Affine.Simplex.pointsWithCircumcenter_point

added def Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter

added theorem Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter

added theorem Affine.Simplex.sum_centroidWeightsWithCircumcenter

added theorem Affine.Simplex.sum_circumcenterWeightsWithCircumcenter

added theorem Affine.Simplex.sum_pointWeightsWithCircumcenter

added theorem Affine.Simplex.sum_pointsWithCircumcenter

added theorem Affine.Simplex.sum_reflectionCircumcenterWeightsWithCircumcenter

added theorem AffineIndependent.existsUnique_dist_eq

added theorem EuclideanGeometry.circumcenter_eq_of_cospherical

added theorem EuclideanGeometry.circumcenter_eq_of_cospherical_subset

added theorem EuclideanGeometry.circumradius_eq_of_cospherical

added theorem EuclideanGeometry.circumradius_eq_of_cospherical_subset

added theorem EuclideanGeometry.circumsphere_eq_of_cospherical

added theorem EuclideanGeometry.circumsphere_eq_of_cospherical_subset

added theorem EuclideanGeometry.cospherical_iff_exists_mem_of_complete

added theorem EuclideanGeometry.cospherical_iff_exists_mem_of_finiteDimensional

added theorem EuclideanGeometry.dist_eq_iff_dist_orthogonalProjection_eq

added theorem EuclideanGeometry.dist_set_eq_iff_dist_orthogonalProjection_eq

added theorem EuclideanGeometry.eq_or_eq_reflection_of_dist_eq

added theorem EuclideanGeometry.existsUnique_dist_eq_of_insert

added theorem EuclideanGeometry.exists_circumcenter_eq_of_cospherical

added theorem EuclideanGeometry.exists_circumcenter_eq_of_cospherical_subset

added theorem EuclideanGeometry.exists_circumradius_eq_of_cospherical

added theorem EuclideanGeometry.exists_circumradius_eq_of_cospherical_subset

added theorem EuclideanGeometry.exists_circumsphere_eq_of_cospherical

added theorem EuclideanGeometry.exists_circumsphere_eq_of_cospherical_subset

added theorem EuclideanGeometry.exists_dist_eq_iff_exists_dist_orthogonalProjection_eq