Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-19 19:45 640ba6c8

View on Github →

feat(geometry/euclidean): cospherical points (#4178) Define cospherical points in a Euclidean space (the general-dimension version of the two-dimensional concept of a set of points being concyclic) and prove some very basic lemmas about them.

Estimated changes

Modified src/geometry/euclidean/basic.lean

added def euclidean_geometry.cospherical

added theorem euclidean_geometry.cospherical_def

added theorem euclidean_geometry.cospherical_empty

added theorem euclidean_geometry.cospherical_insert_singleton

added theorem euclidean_geometry.cospherical_singleton

added theorem euclidean_geometry.cospherical_subset

Modified src/geometry/euclidean/circumcenter.lean

added theorem euclidean_geometry.circumcenter_eq_of_cospherical

added theorem euclidean_geometry.circumcenter_eq_of_cospherical_subset

added theorem euclidean_geometry.circumradius_eq_of_cospherical

added theorem euclidean_geometry.circumradius_eq_of_cospherical_subset

added theorem euclidean_geometry.cospherical_iff_exists_mem_of_complete

added theorem euclidean_geometry.cospherical_iff_exists_mem_of_finite_dimensional

added theorem euclidean_geometry.exists_circumcenter_eq_of_cospherical

added theorem euclidean_geometry.exists_circumcenter_eq_of_cospherical_subset

added theorem euclidean_geometry.exists_circumradius_eq_of_cospherical

added theorem euclidean_geometry.exists_circumradius_eq_of_cospherical_subset