Concyclic points

Definition

Let $S$ be a set of points of the Euclidean space $\mathbb{R}^n$, and let $d$ be the Euclidean distance. The points of $S$ are concyclic if they lie on one circle. That is, there are a plane $P$ that contains $S$, a point $c \in P$ and a real number $r \geq 0$ with $d(x, c) = r$ for each $x \in S$.

Remarks

Three points that are not collinear are always concyclic. Thus each triangle has a circumcircle. Four or more points of the plane are not concyclic in general. Four concyclic points are the vertices of a cyclic quadrilateral. The centre $c$ is on the perpendicular bisector of each two distinct points of $S$. Mathlib's EuclideanGeometry.Concyclic asks for points that are cospherical and coplanar. This is the same condition.

Explanations

L1 human

Concyclic points are points on one common circle. The four corners of a rectangle are concyclic: the circle has its centre at the crossing of the diagonals. The four points $(0, 0)$, $(1, 0)$, $(2, 0)$ and $(0, 1)$ are not concyclic, because a circle meets a line in at most two points.